{"id":{"repo_id":"radboud","oai_identifier":"oai:repository.ubn.ru.nl:2066/18729"},"canonical_url":"https://search.dev.ndltd.org/etd/radboud/oai:repository.ubn.ru.nl:2066/18729","repository":{"repo_id":"radboud","name":"Radboud University Nijmegen","base_url":"https://repository.ubn.ru.nl/oai/request"},"display":{"title":"Studies in mechanical verification of mathematical proofs","abstract":"Contains fulltext : 18727_studinmev.pdf (Publisher’s version ) (Open Access)","abstract_html":"Contains fulltext : 18727_studinmev.pdf (Publisher’s version ) (Open Access)","abstract_has_math":false,"creators":["Ruys, Mark Pieter Jan"],"institution":"[S.l. : s.n.]","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":1999,"date_issued":"1999","date_published":"1999","updated_at":"2026-07-24T04:03:01Z","subjects":[],"languages":["en"],"rights":["(c) Mark Pieter Jan Ruys, 1999"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["9090126449"],"render_values":[{"text":"9090126449","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2066/18729","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Ruys, Mark Pieter Jan"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["1999"]},{"key":"dc:publisher","label":"Institution","values":["[S.l. : s.n.]"]},{"key":"dc:type","label":"Dc Type","values":["Doctoral thesis"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["(c) Mark Pieter Jan Ruys, 1999"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://repository.ubn.ru.nl//bitstream/handle/2066/18729/18727_studinmev.pdf","http://hdl.handle.net/2066/18729","9090126449"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Contains fulltext : 18727_studinmev.pdf (Publisher’s version ) (Open Access)","This thesis is about proof checking in type theory. We will investigate the question how to mechanically verify mathematical proofs. The computer systems we consider are based on a type-theoretical framework. The method we follow is to develop a few representative case studies. This gives us the experience to draw conclusions and to give recommendations. In order to formalize the theorems presented in the case studies, we first have to develop a library of formalized mathematics. We will do this from scratch. During this development we will encounter several choices to make and problems to solve. One particular problem, namely equational reasoning, is studied in more depth and a method for dealing with it in a convenient way is presented in a separate chapter","X, 133 p."]},{"key":"dc:title","label":"Title","values":["Studies in mechanical verification of mathematical proofs"]}]}],"canonical_facts":{"dc:creator":["Ruys, Mark Pieter Jan"],"dc:date":["1999"],"dc:description":["Contains fulltext : 18727_studinmev.pdf (Publisher’s version ) (Open Access)","This thesis is about proof checking in type theory. We will investigate the question how to mechanically verify mathematical proofs. The computer systems we consider are based on a type-theoretical framework. The method we follow is to develop a few representative case studies. This gives us the experience to draw conclusions and to give recommendations. In order to formalize the theorems presented in the case studies, we first have to develop a library of formalized mathematics. We will do this from scratch. During this development we will encounter several choices to make and problems to solve. One particular problem, namely equational reasoning, is studied in more depth and a method for dealing with it in a convenient way is presented in a separate chapter","X, 133 p."],"dc:identifier":["https://repository.ubn.ru.nl//bitstream/handle/2066/18729/18727_studinmev.pdf","http://hdl.handle.net/2066/18729","9090126449"],"dc:language":["en"],"dc:publisher":["[S.l. : s.n.]"],"dc:rights":["(c) Mark Pieter Jan Ruys, 1999"],"dc:title":["Studies in mechanical verification of mathematical proofs"],"dc:type":["Doctoral thesis"]},"updated_at":"2026-07-24T04:03:01Z"}