Mendler, Paul Francis2007-04-232007-04-231987-09http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-870https://hdl.handle.net/1813/6710Type theories can provide a foundational account of constructive mathematics, and for the computer scientist, they can also serve the dual roles of specification and programming languages. In the search for natural and expressive extensions to the NuPrl type theory, we are lead to consider forms of inductive and co-inductive definition. We realize these notions through the addition of two new type constructors, denoted $\mu and \nu$. This represents a step towards a more expressive theory, without adopting a completely impredicative notion of type. With these constructors we can define all the common inductive data types, from natural numbers to infinite trees. Through the propositions-as-types principle, these type constructors yield inductively defined propositions. The induction principle associated with the $\mu$ types lets us define well-founded recursive functions, and dual principle for the $\nu$ types lets us inductively define their "infinite" elements. We present another induction principle for the $\mu$ types which takes advantage of the information hiding properties of the $\{ __ | __ \}$ type, and can be used to define an unbounded search operator, or more generally, to compute not with elements of the $\mu$ type, but under the assumption of its inhabitation. After presenting the proof rules for these new type constructors we give a semantic account, from which intuitionistic consistency is a consequence. First, we consider the the question of inductive types in the simpler setting of the second-order lambda calculus, where we prove a strong normalization property. We also consider typing terms in the presence of type constraints, and present a condition on the constraints (of polynomial complexity in the size of the constraints) for determining if the terms will be strongly normalizable or there will be a diverging typed term. Second, we develop a semantic account of the basic type theory, then relativize it to account for the impredicativity inherent in the definition of the new type constructors. We also show how this model can justify other impredicative type constructors, such as an impredicative type abstraction operation.6773607 bytes1433210 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report