Equality, Quasi-Implicit Products, and Large Eliminations

Vilhelm Sjöberg
(University of Pennsylvania)
Aaron Stump
(The University of Iowa)

This paper presents a type theory with a form of equality reflection: provable equalities can be used to coerce the type of a term. Coercions and other annotations, including implicit arguments, are dropped during reduction of terms. We develop the metatheory for an undecidable version of the system with unannotated terms. We then devise a decidable system with annotated terms, justified in terms of the unannotated system. Finally, we show how the approach can be extended to account for large eliminations, using what we call quasi-implicit products.

In Elaine Pimentel, Betti Venneri and Joe Wells: Proceedings Fifth Workshop on Intersection Types and Related Systems (ITRS 2010), Edinburgh, U.K., 9th July 2010, Electronic Proceedings in Theoretical Computer Science 45, pp. 90–100.
Published: 21st January 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.45.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org