Noam Zeilberger
Assistant Professor in Computer Science 
Laboratoire d'informatique de l'École Polytechnique 
email: noam.zeilberger@polytechnique.edu (or @gmail.com) 
background

interests

news

papers

talks

dissertation

software

students

teaching

etc
Background
I am an assistant professor at LIX and a member of the PARTOUT team within the Proofs and Algorithms pole.
Previously, I was a Birmingham Fellow at the University of Birmingham for three years, and a member of the vibrant Theory Group in the School of Computer Science.
I moved back to France in 2020 to rejoin my wife, after a few years of tricky navigation between Birmingham and Paris.
Before that, 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 MSRInria Joint Centre and as a member of Team Parsifal.
And before all that I was a PhD student at CMU SCS, spending six great years in Pittsburgh, Pennsylvania.
Research Interests
I am interested broadly in connections between logic, language, mathematics, and computation, and my specific focuses of attention have shifted over the years as I've gone down different rabbitholes.
During my PhD studies I fell in love with ideas from programming languages theory, proof theory, and type theory, which later evolved into a love for category theory and an appreciation for combinatorics (especially map theory, using "map" in the sense of the "four color map theorem") and automata theory.
I do like theory!
But also concrete examples, diagrams, and computations.
Recent and Upcoming News and Events (circa mid2023)
Our ANR project LambdaComb is ongoing! You can visit the project page to find out more about this "cartographic quest between lambdacalculus, logic, and combinatorics".
I am very proud of my now former PhD students, Nicolas Blanco and Alexandros Singh, who both recently defended their dissertations!
Recent and notsorecent papers
 Convolution Products on Double Categories and Categorification of Rule Algebras.
 With Nicolas Behr and PaulAndré Melliès.
In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023).
[doi]
 Parsing as a lifting problem and the ChomskySchützenberger representation theorem.
 With PaulAndré Melliès.
In Proceedings of the 38th Conference on Mathematical Foundations of Programming Semantics (MFPS 2022).
[hal] [arXiv:2212.09060]
 Asymptotic Distribution of Parameters in Trivalent Maps and Linear Lambda Terms.
 With Olivier Bodini and Alexandros Singh.
[arXiv:2106.08291]
 Deductive systems and coherence for skew prounital closed categories.
 With Tarmo Uustalu and Niccolò Veltri.
Proceedings of the 15th International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2020).
[arXiv:2102.03809]
 Proof theory of partially normal skew monoidal categories.
 With Tarmo Uustalu and Niccolò Veltri.
In Proceedings of the 3rd Applied Category Theory Conference (ACT 2020).
[arXiv:2101.10487]
 Bifibrations of polycategories and classical linear logic.
 With Nicolas Blanco.
In Proceedings of the 36th Conference on Mathematical Foundations of Programming Semantics (MFPS 2020).
[doi]
 EilenbergKelly reloaded.
 With Tarmo Uustalu and Niccolò Veltri.
In Proceedings of the 36th Conference on Mathematical Foundations of Programming Semantics (MFPS 2020).
[doi]
 The sequent calculus of skew monoidal categories (extended version).
 With Tarmo Uustalu and Niccolò Veltri. To appear in Lambek Memorial Volume, C. Casadio and P. J. Scott (editors), Outstanding Contributions to Logic, Springer, 2020.
[arXiv:2003.05213] [Agda code]
 A sequent calculus for a semiassociative law (extended version).
 Logical Methods in Computer Science, volume 15, issue 1, 2019, pp. 9:19:23. Appeared 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 3valent 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 semiassociative 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.
Electronic Journal of Combinatorics, volume 26, issue 4, 2019. [doi]
 A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine.
 With PaulAndré Melliès. In Proceedings of the ThirtyFirst 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 PaulAndré Melliès. Mathematical Structures in Computer Science 28:6, 736774, 2018. [doi] [arXiv:1501.05115]
 Balanced polymorphism and linear lambda calculus.
 Presented at TYPES 2015.
 Functors are Type Refinement Systems.
 With PaulAndré Melliès. In Proceedings of the 42nd ACM SIGPLANSIGACT 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. 139. [doi] [arXiv:1408.5028]
 Type refinement and monoidal closed bifibrations.

With PaulAndré Melliès. October 1, 2013. [arXiv:1310.0263]
 Polarity and the logic of delimited continuations.

In Proceedings of the TwentyFifth Annual IEEE Symposium on Logic in Computer Science (LICS 2010). [doi] [twelf code] [slides]
 Defunctionalizing focusing proofs.

Presented at the 2009 International Workshop on ProofSearch 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 TwentyThird Annual IEEE Symposium on Logic in Computer Science (LICS 08).
[doi] [tech report]
 Focusing and higherorder abstract syntax.

In Proceedings of the 35th Annual ACM SIGPLANSIGACT 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]
Recent and notsorecent talks
 Generalizing and abstracting the notion of contextfree language
 June 28, 2023, at the Lambda Pros day.
 Type refinement systems: combining intrinsic and extrinsic views of typing, categorically
 December 7, 2022, at the 3rd online workshop on Proofs, Computation and Meaning.
 Type refinement as a unifying principle.
 August 1, 2022, for the Special Session for Frank Pfenning jointly organized by LFMTP and FSCD at FLoC 2022.
 Parsing as a lifting problem and the ChomskySchützenberger representation theorem.
 June 30, 2022, for the Topos Institute Colloquium. [video] [2022.07.21 version at the CMU POP seminar] [2023.04.21 version, invited talk at Journée GT DAAL 2023]
 A quick introduction to species, operads, and closed multicategories.
 Apr 11, 2022, at the LambdaComb kickoff meeting.
 A cartographic quest between lambda calculus, logic, and combinatorics.
 Mar 17, 2022, at the LIX Seminar.
 Fibrational views on typing, proving, and parsing.
 Sep 1, 2021, at the special session on Categorical Type Theory at MFPS 2021.
 Complexity of normalization for subsystems of untyped linear lambda calculus.
 June 28, 2021, at the Structure meets Power Workshop. Warning: We realized (~Nov 2022) that our proof of PTIMEhardness contains a gap! The complexity of normalizing planar lambda terms remains open...
 Skew monoidal categories and the prooftheoretic anatomy of associativity (and unitality).
 February 9, 2021, at the Bath Mathematical Foundations Seminars.
 Untyped Linear Lambda Calculus and the Combinatorics of 3valent graphs.
 December 2, 2020, contributed talk at Combinatorics and Arithmetic for Physics: special days (CAP7). [video]
 Higher connectivity in linear lambdaterms as 3valent graphs.
 September 4, 2019, invited talk at the Fifth Symposium on Compositional Structures (SYCO 5).
 A prooftheoretic analysis of the rotation lattice of binary trees.
 January 9, 2019, joint CombiParsifal seminar at École Polytechnique.
 A prooftheoretic 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 3valent 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.
 Skewclosed objects, typings of linear lambda terms, and flows on trivalent graphs.
 September 9, 2017, at STRING 2017.
 A sequent calculus for a semiassociative 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 29July 2, 2016.
 Linear lambda calculus and the combinatorics of embedded graphs.

October 14, 2015, at Journées Nationales GEOCALLACLTP 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 typetheoretic understanding of zeroknowledge.

September 9, 2012, at the 1st ACM SIGPLAN workshop on HigherOrder 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 noncommutative 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 PaulAndré 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.
Dissertation
PhD in computer science, 2009, Carnegie Mellon University
The Logical Basis of Evaluation Order and PatternMatching.
Committee:
Peter Lee (coadvisor),
Frank Pfenning (coadvisor),
Robert W. Harper,
PaulAndré Melliès (external member)
Techniques from linear logic and infinitary proof theory (connected to the old
idea of a "prooftheoretic semantics" of logic) yield new insights
into seemingly extralogical features of modern programming languages.
By applying the CurryHoward 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 builtin support for
patternmatching. This framework provides an elegant, uniform account of
both untyped and intrinsically welltyped computation, and moreover can
be extended with an extrinsic (Currystyle) 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.
Software
 LinLam
 a Haskell library for experimental linear lambda calculus.
Students
 Former PhD students

 Nicolas Blanco
 Bifibrations of polycategories and classical multiplicative linear logic
 School of Computer Science, University of Birmingham, February 2023.
 Coadvised with Paul Levy.
 Alexandros Singh
 A unified approach to the combinatorics of the λcalculus and maps: bijections and limit properties
 Laboratoire d’Informatique de Paris Nord, Université Paris XIII, November 2022.
 Coadvised with Olivier Bodini.
 Former Masters students

 George Kaye: a visualiser for lambdaterms as rooted maps (MSci project, 2019)
 Tingyu Huang: visualization of combinatorial maps (MSc project, 2019)
 Farzad Jafarrahmani: categorical semantics of induction and subtyping (M2 internship, 2019)
Teaching
 Current DIX
 CSE102  Computer Programming
 CSE301  Functional Programming
 INF412  Fondements de l’Informatique: logique, modèles, calculs
 Former DIX
 CSE103  Introduction to Algorithms
 INF371  Mécanismes de la programmation orientéeobjet
 Former Birmingham
 Functional Programming
 Advanced Topics in Functional Programming
 Introduction to Mathematics for Computer Science
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 truelife 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.
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