Polynomial-time Martin-Lof type theory

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ω. 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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Mathematics

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2011

Author dc:creator

• Pe, Joseph Lim

Contributors dc:contributor

• Henson, C. Ward

• Mathematics
• Computer Science

Statement dc:rights

• Copyright 1991 Pe, Joseph Lim

Language dc:language

eng

Identifier

AAI9210949
(UMI)AAI9210949

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/21156