Skip to main content
PRL Project

A Type Theory with Partial Equivalence Relations as Types

by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli

Presented at TYPES 2014: Types for Proofs and Programs, in Paris, France.

Unofficial PDF


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.