@Inproceedings{EPTCS76.9, author = {Sj\"oberg, Vilhelm and Casinghino, Chris and Ahn, Ki Yung and Collins, Nathan and Eades III, Harley D. and Fu, Peng and Kimmell, Garrin and Sheard, Tim and Stump, Aaron and Weirich, Stephanie}, year = {2012}, title = {Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems}, editor = {Chapman, James and Levy, Paul Blain}, booktitle = {{\rm Proceedings Fourth Workshop on} Mathematically Structured Functional Programming, {\rm Tallinn, Estonia, 25 March 2012}}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {76}, publisher = {Open Publishing Association}, pages = {112-162}, doi = {10.4204/EPTCS.76.9}, }