Electronic Proceedings in Theoretical Computer Science (Feb 2012)

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

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

DOI
https://doi.org/10.4204/EPTCS.76.9
Journal volume & issue
Vol. 76, no. Proc. MSFP 2012
pp. 112 – 162

Abstract

Read online

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.