Irrelevance, heterogeneous equality, and call-by-value dependent type systems

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

Research output: Contribution to journalConference articlepeer-review

14 Scopus citations


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.

Original languageEnglish (US)
Pages (from-to)112-162
Number of pages51
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
StatePublished - Feb 11 2012
Externally publishedYes
Event4th Workshop on Mathematically Structured Functional Programming, MSFP 2012 - Tallinn, Estonia
Duration: Mar 25 2012 → …

ASJC Scopus subject areas

  • Software

Cite this