Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Programming Languages
2012-02-15 v1
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.
Cite
@article{arxiv.1202.2923,
title = {Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems},
author = {Vilhelm Sjöberg and Chris Casinghino and Ki Yung Ahn and Nathan Collins and Harley D. Eades and Peng Fu and Garrin Kimmell and Tim Sheard and Aaron Stump and Stephanie Weirich},
journal= {arXiv preprint arXiv:1202.2923},
year = {2012}
}
Comments
In Proceedings MSFP 2012, arXiv:1202.2407