{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/21156"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/21156","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Polynomial-time Martin-Lof type theory","abstract":"Fragments of extensional Martin-Lof type theory without universes, $ML\\sb0,$ are introduced that conservatively extend S. A. Cook and A. Urquhart's $IPV\\sp\\omega.$ A model for these restricted theories is obtained by interpretation in Feferman's theory APP of operators, a natural model of which is the class of partial recursive functions. In conclusion, an example in group theory is considered.","abstract_html":"Fragments of extensional Martin-Lof type theory without universes, $ML\\sb0,$ are introduced that conservatively extend S. A. Cook and A. Urquhart&#x27;s <span class=\"etd-inline-math\">IPV\\sp&omega;.</span> A model for these restricted theories is obtained by interpretation in Feferman&#x27;s theory APP of operators, a natural model of which is the class of partial recursive functions. In conclusion, an example in group theory is considered.","abstract_has_math":true,"creators":["Pe, Joseph Lim"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Mathematics","degree_department":null,"school":null,"contributors":["Henson, C. Ward"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-05-07T13:00:00Z","date_published":"2011-05-07T13:00:00Z","updated_at":"2026-07-22T22:25:17Z","subjects":["Mathematics","Computer Science"],"languages":["eng"],"rights":["Copyright 1991 Pe, Joseph Lim"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI9210949","(UMI)AAI9210949"],"render_values":[{"text":"AAI9210949","href":null,"code":true},{"text":"(UMI)AAI9210949","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2142/21156","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Henson, C. Ward"]},{"key":"dc:creator","label":"Author","values":["Pe, Joseph Lim"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-05-07T13:00:00Z","10000-01-01","1991"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Mathematics"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Mathematics","Computer Science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 1991 Pe, Joseph Lim"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["AAI9210949","(UMI)AAI9210949","http://hdl.handle.net/2142/21156"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Fragments of extensional Martin-Lof type theory without universes, $ML\\sb0,$ are introduced that conservatively extend S. A. Cook and A. Urquhart's $IPV\\sp\\omega.$ A model for these restricted theories is obtained by interpretation in Feferman's theory APP of operators, a natural model of which is the class of partial recursive functions. In conclusion, an example in group theory is considered.","$IPV\\sp\\omega$ is a higher-order arithmetic that conservatively extends Cook's equational system PV. PV formalizes the notion of feasibly (i.e., polynomial-time verifiably) constructive proof. $IPV\\sp\\omega$ in turn captures a basic notion of polynomial-time computability for functionals of finite (linear) type as well. However, while $IPV\\sp\\omega$ formalizes feasibly constructive first-order number theory, it does not naturally apply to higher mathematics, e.g., in general, it lacks the relation of equality among objects of the same type. This motivates the study of extensions of $IPV\\sp\\omega$ in more expressive formalisms.","$ML\\sb0$ is a predicative intuitionistic type theory based on the propositions-as-types paradigm which identifies a proposition with the set of its proofs. The fragments of $ML\\sb0$ obtained extend the above notions for the polymorphic Martin-Lof type structure and exhibit functionals encoding proofs of theorems. Because of their richness, they are well-suited for the development of feasibly constructive mathematics, particularly in the synthesis of feasible algorithms from proofs.","Made available in DSpace on 2011-05-07T13:00:00Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 9210949.pdf: 2954353 bytes, checksum: 8c866796f9931f3fd9b9715e17969ea9 (MD5) Previous issue date: 1991","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T14:48:52Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:22:10-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission","ETDs are only available to UIUC Users without author permission","U of I Only"]},{"key":"dc:title","label":"Title","values":["Polynomial-time Martin-Lof type theory"]}]}],"canonical_facts":{"dc:contributor":["Henson, C. Ward"],"dc:creator":["Pe, Joseph Lim"],"dc:date":["2011-05-07T13:00:00Z","10000-01-01","1991"],"dc:description":["Fragments of extensional Martin-Lof type theory without universes, $ML\\sb0,$ are introduced that conservatively extend S. A. Cook and A. Urquhart's $IPV\\sp\\omega.$ A model for these restricted theories is obtained by interpretation in Feferman's theory APP of operators, a natural model of which is the class of partial recursive functions. In conclusion, an example in group theory is considered.","$IPV\\sp\\omega$ is a higher-order arithmetic that conservatively extends Cook's equational system PV. PV formalizes the notion of feasibly (i.e., polynomial-time verifiably) constructive proof. $IPV\\sp\\omega$ in turn captures a basic notion of polynomial-time computability for functionals of finite (linear) type as well. However, while $IPV\\sp\\omega$ formalizes feasibly constructive first-order number theory, it does not naturally apply to higher mathematics, e.g., in general, it lacks the relation of equality among objects of the same type. This motivates the study of extensions of $IPV\\sp\\omega$ in more expressive formalisms.","$ML\\sb0$ is a predicative intuitionistic type theory based on the propositions-as-types paradigm which identifies a proposition with the set of its proofs. The fragments of $ML\\sb0$ obtained extend the above notions for the polymorphic Martin-Lof type structure and exhibit functionals encoding proofs of theorems. Because of their richness, they are well-suited for the development of feasibly constructive mathematics, particularly in the synthesis of feasible algorithms from proofs.","Made available in DSpace on 2011-05-07T13:00:00Z (GMT). No. of bitstreams: 2 license.txt: 4922 bytes, checksum: 910b249b4beec47e7ab768910c8f966f (MD5) 9210949.pdf: 2954353 bytes, checksum: 8c866796f9931f3fd9b9715e17969ea9 (MD5) Previous issue date: 1991","Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Howard Ding (hding2@illinois.edu) on 2011-05-07T14:48:52Z Item is restricted indefinitely.","Restriction data tranferred 2014-07-01T11:22:10-05:00 Original Data Group with Access UIUC Users [automated] Release Date: none Reason: ETDs are only available to UIUC Users without author permission","ETDs are only available to UIUC Users without author permission","U of I Only"],"dc:identifier":["AAI9210949","(UMI)AAI9210949","http://hdl.handle.net/2142/21156"],"dc:language":["eng"],"dc:rights":["Copyright 1991 Pe, Joseph Lim"],"dc:subject":["Mathematics","Computer Science"],"dc:title":["Polynomial-time Martin-Lof type theory"],"dc:type":["text"],"thesis:degree_discipline":["Mathematics"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:17Z"}