Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems

Sjöberg, Vilhelm; Casinghino, Chris; Ahn, Ki Yung; Collins, Nathan; Eades III, Harley D.; Fu, Peng; Kimmell, Garrin; Sheard, Tim; Stump, Aaron; Weirich, Stephanie

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems

Vilhelm Sjöberg
(University of Pennsylvania)

Chris Casinghino
(University of Pennsylvania)

Ki Yung Ahn
(Portland State University)

Nathan Collins
(Portland State University)

Harley D. Eades III
(University of Iowa)

Peng Fu
(University of Iowa)

Garrin Kimmell
(University of Iowa)

Tim Sheard
(Portland State University)

Aaron Stump
(University of Iowa)

Stephanie Weirich
(University of Pennsylvania)

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.

In James Chapman and Paul Blain Levy: Proceedings Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012), Tallinn, Estonia, 25 March 2012, Electronic Proceedings in Theoretical Computer Science 76, pp. 112–162.
Published: 11th February 2012.

ArXived at: https://dx.doi.org/10.4204/EPTCS.76.9	bibtex	PDF

References in reconstructed bibtex, XML and HTML format (approximated).

Comments and questions to:

eptcs@eptcs.org

For website issues:

webmaster@eptcs.org