Noam Zeilberger

email: [noam.zeilberger] at | [zeilbern] at
office hours (UG37): Wed 13:00-15:00 (or by appointment)
office phone: x58199

Since October 2016, I am Birmingham Fellow at the University of Birmingham, and a member of the Theory Group within the School of Computer Science.

Before arriving at Rummidge, I was an itinerant postdoc for around seven years, first in Paris at Laboratoire PPS (now IRIF) with a fellowship of the Fondation Sciences Mathématiques de Paris, then at IMDEA Software in Madrid, then at the Institute for Advanced Study in Princeton (during the special year on Univalent Foundations), and then back to Paris at the MSR-Inria Joint Centre and as a member of Team Parsifal. Before all that I was a PhD student at CMU SCS, spending six great years in Pittsburgh, Pennsylvania.

interests | news | papers | talks | dissertation | old papers | etc

Research Interests

I am interested broadly in connections between logic, language, and computation. More specifically, in my research I strive to identify and understand the basic mathematical structures underlying the design, implementation, and analysis of programming languages, using tools such as category theory and proof theory. More generally, I am interested in how all this fits within the broader world of mathematics and computer science.

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 (and as an unexpected side effect of the above project) I have also been very interested in understanding some striking connections between lambda calculus and combinatorics, particularly the combinatorics of maps first worked out by Bill Tutte. (The term "map" has different senses in mathematics, but here it is meant in the cartographic sense of a subdivision of a surface into regions.) You can have a look at my talk on Lambda Calculus and the 4CT for a quick introduction to this fascinating world.

An older interest I have is in the notion of zero-knowledge proof from cryptography/complexity theory, 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".

If you are interested in PhD research on any of these or related topics, please contact me. Note that the department has PhD studentships available.

Recent and Upcoming News and Events

  • 1-2 July 2019: attending CLA 2019 in Versailles.
  • 14-18 April 2019: I will be teaching a course on type refinement systems at the Midlands Graduate School.
  • 16-19 January 2019: attending POPL 2019 and OBT 2019.
  • 26-29 November 2018: attending Shonan meeting on Diagrammatic methods for linear and nonlinear systems.
  • 24-25 October 2018: attending Combinatorics and Arithmetic for Physics at IHES.
  • 1 October 2018: welcome to Nicolas Blanco, who will be starting a PhD with me at the University of Birmingham!
  • 10-23 September 2018: East Coast tour (attending VVMC and Harperfest, giving talks at Rutgers, Wesleyan, and Buffalo).
  • 7-12 July 2018: attending FLOC in Oxford, and presenting "A theory of linear typings as flows on 3-valent graphs" at LICS 2018.
  • 22 June 2018: speaking at the OASIS seminar in Oxford.
  • 19 June 2018: participating in the workshop on Practical and Foundational Aspects of Type Theory at the University of Kent.
  • 24-25 May 2018: attending CLA 2018 and speaking on "A sequent calculus for a semi-associative law".
  • 27 March 2018: finished preparing an extended version of "A sequent calculus for a semi-associative law", now including a proof of the lattice property!
  • Recent papers and drafts

    A sequent calculus for a semi-associative law (extended version).
    Logical Methods in Computer Science, volume 15, issue 1, 2019, pp. 9:1-9:23. To appear in a special issue of selected papers from FSCD 2017. [journal link] [arXiv:1803.10080]. [some related code]
    Two Questions about the Fractional Counting of Partitions.
    With Doron Zeilberger. October 30, 2018. [paper url] [arXiv:1810.12701].
    The sequent calculus of skew monoidal categories.
    With Tarmo Uustalu and Niccolò Veltri. In Proceedings of the 34th Conference on Mathematical Foundations of Programming Semantics (MFPS 2018). [paper url with Agda code]
    A theory of linear typings as flows on 3-valent graphs.
    In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018). [doi] [arXiv:1804.10540]
    A sequent calculus for a semi-associative law.
    In Proceedings of the Second International Conference on Formal Structures for Computation and Deduction (FSCD 2017). [Note this article mostly supersedes arXiv:1701.02917, and is superseded by arXiv:1803.10080.]
    Connected chord diagrams and bridgeless maps.
    With Julien Courtiel and Karen Yeats. November 14, 2016. [arXiv:1611.04611]
    A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine.
    With Paul-André Melliès. In Proceedings of the Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016). [doi] [arXiv:1601.06098]
    Towards a mathematical science of programming.
    Research statement, circa 2016.
    Linear lambda terms as invariants of rooted trivalent maps.
    Journal of Functional Programming, volume 26, 2016. [doi] [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. Mathematical Structures in Computer Science 28:6, 736-774, 2018. [doi] [arXiv:1501.05115]
    Balanced polymorphism and linear lambda calculus.
    Presented at TYPES 2015.
    Functors are Type Refinement Systems.
    With Paul-André Melliès. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (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. [doi] [arXiv:1408.5028]
    Type refinement and monoidal closed bifibrations.
    With Paul-André Melliès. October 1, 2013. [arXiv:1310.0263]

    Recent talks

    Higher connectivity in linear lambda-terms as 3-valent graphs.
    September 4, 2019, invited talk at the Fifth Symposium on Compositional Structures (SYCO 5).
    A proof-theoretic analysis of the rotation lattice of binary trees.
    January 9, 2019, joint Combi-Parsifal seminar at École Polytechnique.
    A proof-theoretic analysis of the rotation lattice of binary trees.
    September 13, 2018, at the Rutgers Experimental Mathematics Seminar.
    A theory of linear typings as flows on 3-valent graphs.
    July 9, 2018, at LICS 2018.
    Lambda calculus and the Four Colour Theorem.
    June 22, 2018, at the OASIS seminar in Oxford.
    Type refinement systems and the categorical perspective on type theory.
    June 19, 2018, at the workshop on Practical and Foundational Aspects of Type Theory at the University of Kent.
    Lambda calculus and the Four Colour Theorem.
    November 21, 2017, at the Edinburgh LFCS Seminar.
    Skew-closed objects, typings of linear lambda terms, and flows on trivalent graphs.
    September 9, 2017, at STRING 2017.
    A sequent calculus for a semi-associative law.
    September 4, 2017, at FSCD 2017.
    Some bridges between lambda calculus and graphs on surfaces.
    July 6, 2017, at the 26th British Combinatorial Conference.
    Some enumerative, topological, and algebraic aspects of linear lambda calculus.
    May 18, 2017, at CLA 2017.
    A Categorical Perspective on Type Refinement Systems.
    December 9, 2016, at the Logic and Semantics Seminar of the Cambridge Computer Laboratory.
    A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine.
    July 7, 2016, at LICS 2016.
    Principles of Type Refinement.
    Lectures given at OPLSS 2016, June 29-July 2, 2016.
    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.
    Towards a non-commutative logic of effects.
    December 2010, presented at the Oxford OASIS seminar and at MSR Cambridge. As it says on one of the first slides, the ideas here were "X% baked for some X probably significantly below 50". Still, I'm posting the talk here for historical reasons, since this was near the time Paul-André and I first started thinking about substructural types as presheaves over context categories (with helpful exchanges with Jonas!), an idea that eventually developed into our work on type refinement systems. The connection between focusing/polarity and Isbell duality was elaborated upon in our MSCS paper, though I think there is still more to be said.


    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.

    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). [doi] [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). [doi] [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). [doi] [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]

    Et cetera

    Rapport sur la Thèse de Dov Tamari
    Report on the thesis of Dov Tamari, signed by his advisor Paul Dubreil (scanned by phone at Sophie Germain Library).
    nLab and OEIS
    Knowledge is a collaborative effort.
    And Quiet Flows the Mon
    A photography project from the dark days after the 2004 U.S. Presidential Elections. 2017 update: whoops, it seems that my dystopian vision of US politics was a little bit too optimistic!
    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.
    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.

    It would scarcely be an exaggeration to say that the whole of mathematics is enwrapped in these trichotomic graphs; and they will be found extremely pertinent to logic.
    C. S. Peirce

    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