Noam Zeilberger

Post-doctoral researcher	Supported by the Fondation Sciences Mathématiques de Paris
Laboratoire PPS / Equipe pir2
Université Paris 7 - Denis Diderot
work email: n...@pps.jussieu.fr	personal email: n...@gmail.com

NEWS: I have moved to IMDEA Software Madrid.

Research Interests

I am interested in programming languages and logic, and the connection between them known as the propositions-as-types correspondence (or proofs-as-programs, or Curry-Howard, etc.). I am especially interested in type systems that push the boundaries of this correspondence, such as dependent types and refinement types. More generally, I am interested in the interaction of syntax and semantics, in programming languages as well as proof theory, model theory, and games semantics. I use proof assistants (such as Agda, Coq, and Twelf) as mathematical laboratories for experimenting with ideas. I believe that a close connection between theory and practice is both possible and necessary.

Dissertation

PhD in computer science, 2009, Carnegie Mellon University
The Logical Basis of Evaluation Order and Pattern-Matching.
Committee: Peter Lee (co-advisor), Frank Pfenning (co-advisor), Robert W. Harper, Paul-André Melliès (external member)

Techniques from linear logic and infinitary proof theory (connected to the old idea of a "proof-theoretic semantics" of logic) yield new insights into seemingly extra-logical features of modern programming languages. By applying the Curry-Howard correspondence to focusing proofs, we develop a polarized type theory in which evaluation order is explicitly reflected at the level of types, and which has built-in support for pattern-matching. This framework provides an elegant, uniform account of both untyped and intrinsically well-typed computation, and moreover can be extended with an extrinsic (Curry-style) type system to express and enforce more refined semantic properties of programs. We apply these ideas to explore the theory of typing and subtyping for intersection and union types in the presence of effects, giving a simplified explanation of some of the unusual artifacts of existing systems.

Drafts

Publications

Polarity and the logic of delimited continuations.: Presented at LICS 2010. [twelf code] [slides]
Defunctionalizing focusing proofs.: Presented at the 2009 International Workshop on Proof-Search in Type Theories. [twelf code] [more twelf]
Refinement types and computational duality.: In Proceedings of the 2009 Workshop on Programming Languages meets Program Verification (PLPV 09). [agda code]
Focusing on binding and computation.: With Dan Licata and Bob Harper. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 08). [tech report]
Focusing and higher-order abstract syntax.: In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 08). [coq code] [notes]
On the unity of duality.: Annals of Pure and Applied Logic 153:1 (2008), special issue on "Classical logic and computation". [doi]

Other talks

Towards a Non-Commutative Logic of Effects.: December 2-3, 2010, at MSR Cambridge and at the Oxford OASIS Seminar
Symmetry and Asymmetry in Logic (Rereading Dummett through Girard [and vice versa!]).: March 22, 2010, at Proofs and Meaning
Towards a Proof-Theoretic Semantics of Programming.: October 21, 2009, at the Groupe de travail Théorie des types et réalisabilité.
Polarity and duality in type theory.: February 20, 2008 at DTP 08.

Other papers

Soundness of labelled deduction.: August, 2005. An attempt at a constructive proof of the soundness of labelled deduction for intuitionistic logic. This is essentially a variation on the usual "prime context" approach establishing completeness of intuitionistic logic with respect to Kripke semantics, but avoiding proof-by-contradiction, and using the subformula property to stay finitary. For a more novel approach, see Jason Reed and Frank Pfenning's "Intuitionistic letcc via labelled deduction".
Modal BI and Separation Logic.: June, 2005. Describes how to extend the logic of bunched implications with an S4-like box modality, and its relationship to "purity" in separation logic.
Nathack: a natural language interface for nethack.: January, 2003. With Cassia Martin, David Molnar, and Dev Purkayastha. As the title suggests, this was a natural language interface for nethack! Done with a mix of prolog, embedded lua, and scary hacking within nethack's internal C source. Our code is lying around somewhere, and I could dig it up upon request.

Historical documents

Letter from Per Martin-Löf to Michael Dummett, dated 5 March 1976: On Dummett's invitation, Martin-Löf gave a series of eight lectures at Oxford's All Souls College, with Dummett and Dag Prawitz in the audience. This letter (dated shortly before Dummett's 1976 William James Lectures) was accompanied by Peter Hancock's notes on the first half of this series. Thanks to Peter Hancock for the scanned copy.

Et cetera

The Paralyzing Paradoxes of Professor Polaro: My research blog, primarily about proofs and programs
CiteULike: A possibly out-of-date reading list.
Wikipedia editing: Knowledge is a collaborative effort.
And Quiet Flows the Mon: A photography project from the dark days after the 2004 U.S. Presidential Elections.
In Tune With Fun: A true-life story about learning the accordion.

We may just be cockroaches at the base of a very large garbage mountain.
Dana Scott (on mathematics)