Irrelevance, Heterogeneous Equity, and Call-by-value Dependent Type SystemsDepartmental Papers (CIS)
Date of this Version1-1-2012
Document TypeConference Paper
AbstractWe 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 InformationVilhelm Sjoberg, Chris Casinghino, Nathan Collins, Ki Yung Ahn, et al.. "Irrelevance, Heterogeneous Equity, and Call-by-value Dependent Type Systems" (2012)
Available at: http://works.bepress.com/stephanie_weirich/31/