Irrelevance, Heterogeneous Equality, and Call-by-Value Dependent Type Systems
The authors present a full-spectrum dependently typed core language which includes both non-termination and computational irrelevance (a.k.a. erasure), a combination which has not been studied before. The two features interact: to protect type safety they must be careful to only erase terminating expressions. Their language design is strongly influenced by the choice of CBV evaluation, and by their novel treatment of propositional equality which has a heterogeneous, completely erased elimination form. The Trellys project is a collaborative effort to design a new dependently typed programming language. Their goal is to bridge the gap between ordinary functional programming and program verification with dependent types.