Equality, Quasi-Implicit Products, and Large Eliminations

by Vilhelm Sjöberg, Aaron Stump
Published 2011-01-01

Termination Casts: A Flexible Approach to Termination with General Recursion

by Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich
Published 2010-12-01

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