Inductive Definition in Type Theory
No Access Until
Permanent Link(s)
Collections
Other Titles
Author(s)
Abstract
Type 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