I’m interested in the the connections between logic (especially structural proof theory, type theory and ordinal analysis) and the meta-theory of programming languages. I am especially interested in formalizing techniques that are used proving foundational properties of both logics and programming languages, such as logical relations, transfinite induction and coinduction. Here is my CV.
|email:||MyFirstName.MyLastName@gmail.com (substitute for the appropriate names)|
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.
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.
|2002-2010||Yale University, Department of Computer Science, New Haven, Connecticut, USA.|
|Ph.D. in Computer Science, May 2010.|
|Thesis: Syntactic Finitism in the Metatheory of Programming Languages|
|Advisor: Prof. Carsten Schürmann.|
|2004||Yale University, Department of Computer Science, New Haven, Connecticut, USA.|
|M.S. in Computer Science, May 2004.|
|1998-2002||Carnegie Mellon University, Department of Computer Science, Pittsburgh, Pennsylvania, USA.|
|B.S. in Computer Science (with honors), May 2002.|
|Thesis: The Undecidability of the Finite Refutability of Entailments in Lattice-Theoretic Models of the Lambda Calculus|
|12.2009-6.2011||Postdoc||π r2 Group, INRIA-Rocquencourt Paris-Antenne, Paris, France|
|9.2005-8.2008||Research and Teaching Assistant||PLS Group, ITU Copenhagen, Copenhagen, Denmark|
|6.2001-8.2001||Research Intern||ROPAS Group, KAIST, Daejon, South Korea|
Teaching Experience Teaching Assistant
|IT University of Copenhagen,||Spring 2008||Object-oriented Programming, Introduction.|
|Denmark||Fall 2007||Object-oriented Programming, Introduction.|
|Spring 2007||Object-oriented Programming, Introduction.|
|Fall 2006||Object-oriented Programming.|
|Yale University, USA||Fall 2004||First-Order Logic (Phil 115).|
|Spring 2004||Data Structures and Programming Techniques (CS 223).|
|Fall 2003||Introduction to Computer Science (CS 201).|
|Carnegie Mellon University, USA||Spring 2001||Principles of Programming (15-212)|
This document was translated from LATEX by HEVEA.