Refereed Publications

Jeffrey Sarnat and Carsten Schürmann. Lexicographic path induction. In Proceedings of the 9th Internationl Conference on Typed Lambda Calculi and Applications, Brasìlia, Brazil, 1-3 July 2009, pages 279–293.

Carsten Schürmann and Jeffrey Sarnat. Structural logical relations. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 24-27 June 2008, Pittsburgh, PA, USA, pages 69–80, 2008.

Carsten Schürmann, Adam Poswolsky, and Jeffrey Sarnat. The ∇-calculus. Functional programming with higher-order encodings. In Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications, Nara, Japan, 21-23 April 2005, pages 339–353, 2005.

Dissertation

Jeffrey Sarnat. Syntactic Finitism in the Metatheory of Programming Languages. Yale University Dissertation, May 2010.

Unpublished Technical Reports

Jeffrey Sarnat LFΣ: The Metatheory of LF with Σ Types. Yale Technical Report, 2003.

Carsten Schürmann, Adam Poswolsky, and Jeffrey Sarnat. The ∇-calculus. Functional programming with higher-order encodings. Extended technical report. Yale Technical Report, 2004.