17 citations · 19 across the 3 of their papers we have counts for
3 papers
cs.PL2022
Strong Normalization for the Calculus of Constructions
Chris Casinghino
The calculus of constructions (CC) is a core theory for dependently typed programming and higher-order constructive logic. Originally introduced in Coquand's 1985 thesis, CC has in…
cs.PL2012★ 17 cited
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn +7
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 studi…
cs.PL2012★ 2 cited
Step-Indexed Normalization for a Language with General Recursion
Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich
The Trellys project has produced several designs for practical dependently typed languages. These languages are broken into two fragments-a_logical_fragment where every term normal…