Journal article
Equality, Quasi-Implicit Products, and Large Eliminations
Electronic proceedings in theoretical computer science, Vol.45(45), pp.90-100
01/23/2011
DOI: 10.4204/EPTCS.45.7
Abstract
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.
Details
- Title: Subtitle
- Equality, Quasi-Implicit Products, and Large Eliminations
- Creators
- Vilhelm Sjoberg - University of PennsylvaniaAaron Stump - Association for Computing Machinery
- Resource Type
- Journal article
- Publication Details
- Electronic proceedings in theoretical computer science, Vol.45(45), pp.90-100
- DOI
- 10.4204/EPTCS.45.7
- ISSN
- 2075-2180
- eISSN
- 2075-2180
- Publisher
- Open Publ Assoc
- Number of pages
- 11
- Grant note
- 0910510; 0910786 / U.S. National Science Foundation; National Science Foundation (NSF)
- Language
- English
- Date published
- 01/23/2011
- Academic Unit
- Computer Science
- Record Identifier
- 9984410855602771
Metrics
5 Record Views