Noam Zeilberger

email: [my full name] at gmail.com

Background

  • 2015-: Parsifal Team (Inria), in Palaiseau, France
  • 2013-2015: MSR-Inria Joint Centre, in Palaiseau, France
  • 2012-2013: Institute for Advanced Study, Princeton, NJ
  • 2011-2012: IMDEA Software, in Madrid, Spain
  • 2009-2011: Laboratoire PPS & Equipe πr² on a fellowship of the Fondation Sciences Mathématiques de Paris
  • 2003-2009: PhD studies at CMU SCS, in Pittsburgh, PA

    NEWS: I'm at OPLSS16, giving some lectures on Principles of Type Refinement!

    Research Interests

    I am interested broadly in connections between logic, language, computation, and mathematics.

    A long-running project which I've been collaborating on seeks to develop a common mathematical language that unifies the disparate traditions of Hoare Logic, dependent type theory, and linear logic. One conclusion reached from this project is that the established wisdom about the relationship between type theory and category theory needs to be revised, and that this has important implications for the way we look at type systems and other deductive formalisms. You can find out more about this view in my paper with Paul-André Melliès, "Functors are Type Refinement Systems" (POPL 2015). Turning this vision into a practical reality will require a lot of work, but I'm convinced that the path ahead will be exciting!

    Since more recently, I have been intrigued by a striking connection between lambda calculus and maps, described in a paper with Alain Giorgetti which you can find in "Recent papers and drafts", as well as in a more informal talk I gave at the POPL "Off the Beaten Track" workshop. Again, I think there are many fascinating questions to explore here.

    A different interest I have is in the notion of zero-knowledge proof from cryptography/complexity theory, but in particular how it can be reconciled with notions of knowledge from constructive logic. I gave a talk about these connections at HOPE 2012, which you can find in "Recent talks".

    Recent papers and drafts

    Principles of Type Refinement.
    Lecture notes for OPLSS 2016.
    A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine.
    With Paul-André Melliès.To appear at LICS 2016. [arXiv:1601.06098]
    Linear lambda terms as invariants of rooted trivalent maps.
    December 21, 2015. [arXiv:1512.06751]
    Counting isomorphism classes of β-normal linear lambda terms.
    September 25, 2015. [arXiv:1509.07596]
    An Isbell Duality Theorem for Type Refinement Systems.
    With Paul-André Melliès. Revised version of July 31, 2015 (under submission). [arXiv:1501.05115]
    Balanced polymorphism and linear lambda calculus.
    Presented at TYPES 2015. Full manuscript in preparation.
    Functors are Type Refinement Systems.
    With Paul-André Melliès. Appeared at POPL 2015. [doi]
    A correspondence between rooted planar maps and normal planar lambda terms.
    With Alain Giorgetti. Logical Methods in Computer Science, Vol. 11(3:22)2015, pp. 1-39. [arXiv:1408.5028]
    Type refinement and monoidal closed bifibrations.
    With Paul-André Melliès. October 1, 2013. [arXiv:1310.0263]

    Recent talks

    Linear lambda calculus and the combinatorics of embedded graphs.
    October 14, 2015, at Journées Nationales GEOCAL-LAC-LTP 2015. [pdf]
    Balanced polymorphism and linear lambda calculus.
    May 18, 2015, at TYPES 2015.
    A connection between lambda calculus and maps.
    January 18, 2015, at OBT 2015.
    Functors are Type Refinement Systems.
    January 15, 2015, at POPL 2015
    Polarity in Proof Theory and Programming.
    August 30, 2013, at the Summer School on Linear Logic and Geometry of Interaction in Torino, Italy.
    HOPE for a type-theoretic understanding of zero-knowledge.
    September 9, 2012, at the 1st ACM SIGPLAN workshop on Higher-Order Programming with Effects. (Note: the slides seem to render funny with Firefox -- best viewed in Chrome or Safari.)
    BONUS: slides for the "15 minute" version I gave October 4th at the IAS postdoc seminar series.

    Older publications

    Polarity and the logic of delimited continuations.
    In Proceedings of the Twenty-Fifth Annual IEEE Symposium on Logic in Computer Science (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]

    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.

    Other papers

    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.

    Et cetera

    the nLab
    Knowledge is a collaborative effort.
    And Quiet Flows the Mon
    A photography project from the dark days after the 2004 U.S. Presidential Elections.
    Archive of papers by John Reynolds
    Direct link to the CMU AFS directory, since the ftp server is sometimes down.
    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)

    And tell me Margaret, when I’m gone, what will I want,
    To be left at the bottom of a garbage bin, or dusted off and pulled up onto stage?

    Jason Webley