KnowledgeBase » 
PUBLICATION
» ID = 722
A Type Theory with Partial Equivalence Relations as Types
by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli
2014
Presented at TYPES 2014: Types for Proofs and Programs, in Paris, France.
Abstract
A small core type language with intersection types in which a partial equivalence relation on closed terms is a type is enough to build the non-inductive types of Nuprl, including the types of dependent functions and partial functions. Using induction on natural numbers and intersection types, we build coinductive types; and using partial functions and coinductive types we build algebraic datatypes.