Step-Indexed Normalization for a Language with General Recursion

by Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich
Published 2012-02-01

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

by Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich
Published 2012-02-01