Conference proceeding
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Proceedings Fourth Workshop on Mathematically Structured Functional Programming , pp.112-162
Electronic Proceedings in Theoretical Computer Science (EPTCS), 76
02/13/2012
DOI: 10.4204/EPTCS.76.9
Abstract
We present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studied before. The two features interact: to protect type safety we must be careful to only erase terminating expressions. Our language design is strongly influenced by the choice of CBV evaluation, and by our novel treatment of propositional equality which has a heterogeneous, completely erased elimination form.
Details
- Title: Subtitle
- Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
- Creators
- Vilhelm Sjöberg - University of PennsylvaniaChris Casinghino - University of PennsylvaniaKi Yung Ahn - Portland State UniversityNathan Collins - Portland State UniversityHarley D Eades III - University of IowaPeng Fu - University of IowaGarrin Kimmell - University of IowaTim Sheard - Portland State UniversityAaron Stump - University of IowaStephanie Weirich - University of Pennsylvania
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings Fourth Workshop on Mathematically Structured Functional Programming , pp.112-162
- Series
- Electronic Proceedings in Theoretical Computer Science (EPTCS); 76
- DOI
- 10.4204/EPTCS.76.9
- ISSN
- 2075-2180
- eISSN
- 2075-2180
- Language
- English
- Date published
- 02/13/2012
- Academic Unit
- Computer Science
- Record Identifier
- 9984259415002771
Metrics
28 Record Views