Skip to main content
Irrelevance, Heterogeneous Equity, and Call-by-value Dependent Type Systems
Departmental Papers (CIS)
  • Vilhelm Sjoberg, University of Pennsylvania
  • Chris Casinghino, University of Pennsylvania
  • Nathan Collins, Portland State University
  • Ki Yung Ahn, Portland State University
  • Tim Sheard, Portland State University
  • Harley D Eades, III, University of Iowa
  • Peng Fu, University of Iowa
  • Garrin Kimmell, University of Iowa
  • Aaron Stump, University of Iowa
  • Stephanie Weirich, University of Pennsylvania
Date of this Version
Document Type
Conference Paper

Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, and Stephanie Weirich. Irrelevance, Heterogenous Equality, and Call-by-value Dependent Type Systems. In Fourth workshop on Mathematically Structured Functional Programming (MSFP '12), 2012

Copyright held by the authors.

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.
Citation Information
Vilhelm Sjoberg, Chris Casinghino, Nathan Collins, Ki Yung Ahn, et al.. "Irrelevance, Heterogeneous Equity, and Call-by-value Dependent Type Systems" (2012)
Available at: