Former postdoc in the pi.r2 group of PPS at INRIA-Rocquencourt’s Paris antenne
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.
Contact
| email: | MyFirstName.MyLastName@gmail.com (substitute for the appropriate names) |
| citizenship: | USA |
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.
Education
| 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 |
Research-Related Employment
| 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.