2025Activity reportProject-TeamPARTOUT
RNSR: 201923495K- Research center Inria Saclay Centre at Institut Polytechnique de Paris
- In partnership with:CNRS, Institut Polytechnique de Paris
- Team name: Proof Automation and RepresenTation: a fOundation of compUtation and deducTion
- In collaboration with:Laboratoire d'informatique de l'école polytechnique (LIX)
Creation of the Project-Team: 2019 December 01
Each year, Inria research teams publish an Activity Report presenting their work and results over the reporting period. These reports follow a common structure, with some optional sections depending on the specific team. They typically begin by outlining the overall objectives and research programme, including the main research themes, goals, and methodological approaches. They also describe the application domains targeted by the team, highlighting the scientific or societal contexts in which their work is situated.
The reports then present the highlights of the year, covering major scientific achievements, software developments, or teaching contributions. When relevant, they include sections on software, platforms, and open data, detailing the tools developed and how they are shared. A substantial part is dedicated to new results, where scientific contributions are described in detail, often with subsections specifying participants and associated keywords.
Finally, the Activity Report addresses funding, contracts, partnerships, and collaborations at various levels, from industrial agreements to international cooperations. It also covers dissemination and teaching activities, such as participation in scientific events, outreach, and supervision. The document concludes with a presentation of scientific production, including major publications and those produced during the year.
Keywords
Computer Science and Digital Science
- A2.1. Programming Languages
- A2.2. Compilation
- A4.5. Formal method for verification, reliability, certification
- A7.2. Logic in Computer Science
- A7.2.1. Decision procedures
- A7.2.2. Automated Theorem Proving
- A7.2.3. Interactive Theorem Proving
- A7.2.4. Mechanized Formalization of Mathematics
- A7.3.1. Computational models and calculability
- A8.1. Discrete mathematics, combinatorics
- A8.11. Game Theory
Other Research Topics and Application Domains
- B6.1. Software industry
1 Team members, visitors, external collaborators
Research Scientists
- Lutz Strassburger [Team leader, INRIA, Senior Researcher, HDR]
- Beniamino Accattoli [INRIA, Researcher, HDR]
- Kaustuv Chaudhuri [INRIA, Researcher]
- Dale Miller [INRIA, Senior Researcher, HDR]
- Benjamin Werner [INRIA, Senior Researcher]
Faculty Members
- Ambroise Lafont [ECOLE POLY PALAISEAU, Associate Professor]
- Noam Zeilberger [ECOLE POLY PALAISEAU, Associate Professor]
Post-Doctoral Fellows
- Victoria Barrett [INRIA, Post-Doctoral Fellow, from Sep 2025]
- Victoria Barrett [Inria, Post-Doctoral Fellow, until Aug 2025]
PhD Students
- Farah Al Wardani [Inria]
- Arunava Gantait [ECOLE POLY PALAISEAU]
- Adrienne Lancelot [ECOLE POLY PALAISEAU, from Oct 2025]
- Adrienne Lancelot [INRIA, until Sep 2025]
- Niyousha Najmaei [ECOLE POLY PALAISEAU]
Interns and Apprentices
- Samar Rahmouni [Inria, Intern, from Apr 2025 until Sep 2025]
- Johann Rosain [ENS DE LYON, Intern, from Sep 2025]
Administrative Assistant
- Michael Barbosa [INRIA]
2 Overall objectives
There is an emerging consensus that formal methods must be used as a matter of course in software development. Most software is too complex to be fully understood by one programmer or even a team of programmers, and requires the help of computerized techniques such as testing and model checking to analyze and eliminate entire classes of bugs. Moreover, in order for the software to be maintainable and reusable, it not only needs to be bug-free but also needs to have fully specified behavior, ideally accompanied with formal and machine-checkable proofs of correctness with respect to the specification. Indeed, formal specification and machine verification is the only way to achieve the highest level of assurance (EAL7) according to the ISO/IEC Common Criteria.1
Historically, achieving such a high degree of certainty in the operation of software has required significant investment of manpower, and hence of money. As a consequence, only software that is of critical importance (and relatively unchanging), such as monitoring software for nuclear reactors or fly-by-wire controllers in airplanes, has been subjected to such intense scrutiny. However, we are entering an age where we need trustworthy software in more mundane situations, with rapid development cycles, and without huge costs. For example: modern cars are essentially mobile computing platforms, smart-devices manage our intensely personal details, elections (and election campaigns) are increasingly fully computerized, and networks of drones monitor air pollution, traffic, military arenas, etc. Bugs in such systems can certainly lead to unpleasant, dangerous, or even life-threatening incidents.
The field of formal methods has stepped up to meet this growing need for trustworthy general purpose software in recent decades. Techniques such as computational type systems and explicit program annotations/contracts, and tools such as model checkers and interactive theorem provers, are starting to become standard in the computing industry. Indeed, many of these tools and techniques are now a part of undergraduate computer science curricula. In order to be usable by ordinary programmers (without PhDs in logic), such tools and techniques have to be high level and rely heavily on automation. Furthermore, multiple tools and techniques often need to marshaled to achieve a verification task, so theorem provers, solvers, model checkers, property testers, etc. need to be able to communicate with—and, ideally, trust—each other.
With all this sophistication in formal tools, there is an obvious question: what should we trust? Sophisticated formal reasoning tools are, generally speaking, complex software artifacts themselves; if we want complex software to undergo rigorous formal analysis we must be prepared to formally analyze the tools and techniques used in formal reasoning itself. Historically, the issue of trust has been addressed by means of relativizing it to small and simple cores. This is the basis of industrially successful formal reasoning systems such as Coq, Isabelle, HOL4, and ACL2. However, the relativization of trust has led to a balkanization of the formal reasoning community, since the Coq kernel, for example, is incompatible with the Isabelle kernel, and neither can directly cross-validate formal developments built with the other. Thus, there is now a burgeoning cottage industry of translations and adaptations of different formal proof languages for bridging the gap. A number of proposals have also been made for universal or retargetable proof languages (e.g., Dedukti, ProofCert) so that the cross-platform trust issues can be factorized into single trusted checkers.
Beyond mutual incompatibility caused by relativized trust, there is a bigger problem that the proof evidence that is accepted by small kernels is generally far too detailed to be useful. Formal developments usually occurs at a much higher level, relying on algorithmic techniques such as unification, simplification, rewriting, and controlled proof search to fill in details. Indeed, the most reusable products of formal developments tend to be these algorithmic techniques and associated collections of hand-crafted rules. Unfortunately, these techniques are even less portable than the fully detailed proofs themselves, since the techniques are often implemented in terms of the behaviors of the trusted kernels. We can broadly say that the problem with relativized trust is that it is based on the operational interpretation of implementations of trusted kernels. There still remains the question of meta-theoretic correctness. Most formal reasoning systems implement a variant of a well known mathematical formalism (e.g., Martin-Löf type theory, set theory, higher-order logic), but it is surprising that hardly any mainstream system has a formalized meta-theory.2 Furthermore, formal reasoning systems are usually associated with complicated checkers for side-conditions that often have unclear mathematical status. For example, the Coq kernel has a built-in syntactic termination checker for recursive fixed-point expressions that is required to work correctly for the kernel to be sound. This termination checker evolves and improves with each version of Coq, and therefore the most accurate documentation of its behavior is its own source code. Coq is not special in this regard: similar trusted features exist in nearly every mainstream formal reasoning system.
The Partout project is interested in the principles of deductive and computational formalisms. In the broadest sense, we are interested in the question of trustworthy and verifiable meta-theory. At one end, this includes the well studied foundational questions of the meta-theory of logical systems and type systems: cut-elimination and focusing in proof theory, type soundness and normalization theorems in type theory, etc. The focus of our research here is on the fundamental relationships behind the the notions of computation and deduction. We are particularly interested in relationships that go beyond the well known correspondences between proofs and programs.3 Indeed, interpreting computation in terms of deduction (as in logic programming) or deduction in terms of computation (as in rewrite systems or in model checking) can often lead to fruitful and enlightening research questions, both theoretical and practical.
From another end, Partout works on the question of the essential nature of deductive or computational formalisms. For instance, we are interested in the question of proof identity that attempts to answer the following question: when are two proofs of the same theorem the same? Surprisingly, this very basic question is left unanswered in proof theory, the branch of mathematics that supposedly treats proofs as algebraic objects of interest. We also pay particular attention to the combinatorial and complexity-theoretic properties of the formalisms. Indeed, it is surprising that until very recently the -calculus, which is the de facto basis of every functional programming language, lacked a good complexity-theoretic foundation, i.e., a cost model that would allow us to use the -calculus directly to define complexity classes.
To put trustworthy meta-theory to use, the Partout project also works on the design and implementations of formal reasoning tools and techniques. We study the mathematical principles behind the representations of formal concepts (-terms, proofs, abstract machines, etc.), with the goal of identifying the relationships and trade-offs. We also study computational formalisms such as higher-order relational programming that is well suited to the specification and analysis of systems defined in the structural operational semantics (SOS) style. We also work on foundational questions about induction and co-induction, which are used in intricate combinations in metamathematics.
3 Research program
Software and hardware systems perform computation (systems that process, compute and perform) and deduction (systems that search, check or prove). The makers of those systems express their intent using various frameworks such as programming languages, specification languages, and logics. The Partout project aims at developing and using mathematical principles to design better frameworks for computation and reasoning. Principles of expression are researched from two directions, in tandem:
-
Foundational approaches, from theories to applications: studying fundamental problems of programming and proof theory.
Examples include studying the complexity of reduction strategies in lambda-calculi with sharing, or studying proof representations that quotient over rule permutations and can be adapted to many different logics.
-
Empirical approaches, from applications to theories: studying systems currently in use to build a theoretical understanding of the practical choices made by their designers.
Examples include studying realistic implementations of programming languages and proof assistants, which differ in interesting ways from their usual high-level formal description (regarding of sharing of code and data, for example), or studying new approaches to efficient automated proof search, relating them to existing approaches of proof theory, for example to design proof certificates or to generalize them to non-classical logics.
One of the strengths of Partout is the co-existence of a number of different expertise and points of view. Many dichotomies exist in the study of computation and deduction: functional programming vs logic programming, operational semantics vs denotational semantics, constructive logic vs classical logic, proof terms vs proof nets, etc. We do not identify with any one of them in particular, rather with them as a whole, believing in the value of interaction and cross-fertilization between different approaches. Partout defines its scope through the following core tenets:
- An interest in both computation and logic.
- The use of mathematical formalism as our core scientific method, paired with practical implementations of the systems we study.
- A shared belief in the importance of good design when creating new means of expression, iterating towards simplicity and elegance.
More concretely, the research in Partout will be centered around the following four themes:
- Foundations of proof theory as a theory of proofs. Current proof theory is not a theory of proofs but a theory of proof systems. This has many practical consequences, as a proof produced by modern theorem provers cannot be considered independent from the tool that produced it. A central research topic here is the quest for proof representations that are independent from the proof system, so that proof theory becomes a proper theory of proofs.
- Program Equivalence We intend to use our proof theoretical insights to deepen our understanding of the structure of computer programs by discovering canonical representations for functional programming languages, and to apply these to the problems of program equivalence checking and program synthesis.
- Reasoning with relational specifications of formal systems. Formal systems play a central role for proof checkers and proof assistants that are used for software verification. But there is usually a large gap between the specification of those formal systems in concise informal mathematical language and their implementation in ML or C code. Our research goal is to close that gap.
- Foundations of complexity analysis for functional programs. One of the great merits of the functional programming paradigm is the natural availability of high-level abstractions. However, these abstractions jeopardize the programmer's predictive control on the performance of the code, since many low-level steps are abstracted away by higher-order functions. Our research goal is to regain that control by developing models of space and time costs for functional programs.
4 Application domains
4.1 Automated Theorem Proving
The Partout team studies the structure of mathematical proofs, in ways that often makes them more amenable to automated theorem proving – automatically searching the space of proof candidates for a statement to find an actual proof – or a counter-example.
(Due to fundamental computability limits, fully-automatic proving is only possible for simple statements, but this field has been making a lot of progress in recent years, and is in particular interested with the idea of generating verifiable evidence for the proofs that are found, which fits squarely within the expertise of Partout.)
4.2 Proof-assistants
Our work on the structure of proofs also suggests ways how they could be presented to a user, edited and maintained, in particular in “proof assistants”, automated tool to assist the writing of mathematical proofs with automatic checking of their correctness.
4.3 Programming language design
Our work also gives insight on the structure and properties of programming languages. We can improve the design or implementation of programming languages, help programmers or language implementors reason about the correctness of the programs in a given language, or reason about the cost of execution of a program.
5 Social and environmental responsibility
- Benjamin Werner is an elected member of the executive boards (conseils d'administration) of both Ecole polytechnique (X) and Institut Polytechnique de Paris (IPP)
6 Highlights of the year
- Dominik Kirst is recruted via the Inria CRCN concours
- Dale Miller's book "Proof Theory and Logic Programming: Computation as Proof Search" 19 was published by Cambridge University Press, December 2025.
- Accattoli defended his HDR thesis 20 on May 14, 2025.
- Accattoli, Lancelot, and co-authors had a paper published at POPL 3, one of the flagship conferences of the field.
- A paper by Accattoli and co-authors 10 received the best paper award of the conference.
7 Latest software developments, platforms, open data
7.1 Latest software developments
7.1.1 Abella
-
Keyword:
Proof assistant
-
Functional Description:
Abella is an interactive theorem prover for reasoning about computations given as relational specifications. Abella is particuarly well suited for reasoning about binding constructs.
-
Release Contributions:
This release includes a major refactoring of the Abella documentation generator. Abella developments can now be easily converted into interactive web-based presentations that can be used without having to run Abella by the reader.
This release also fixes a number of outstanding issues with the 2.0.7 and earlier releases. At least two of these fixes involve soundness issues with regard to higher-order arguments.
Abella is now also independently packaged for MacOS (homebrew), FreeBSD, and OpenBSD.
- URL:
-
Contact:
Kaustuv Chaudhuri
-
Participants:
Dale Miller, Gopalan Nadathur, Kaustuv Chaudhuri, Mary Southern, Mattéo Cimini, Yuting Wang, an anonymous participant
-
Partner:
Department of Computer Science and Engineering, University of Minnesota
7.1.2 Actema
-
Name:
Actema
-
Keywords:
Higher-order logic, First-order logic, Proof assistant, GUI (Graphical User Interface), Man-machine interfaces, User Interfaces
-
Functional Description:
This is a new approach, aiming at making the building of formal proofs more intuitive and convenient. The system is currently at a prototype stage. An interfacing with the Coq proof-system has been developed in 2023 and 2024 and is now freely available. The system runs through an html/JS serve.
-
Release Contributions:
This version can be used online at actema.xyz and comes with explanation videos.
- URL:
- Publication:
-
Contact:
Benjamin Werner
-
Participant:
4 anonymous participants
-
Partner:
Ecole Polytechnique
7.1.3 DAMF Dispatch
-
Keywords:
Interactive Theorem Proving, Distributed systems, Verification
-
Scientific Description:
The Distributed Assertion Management Framework (DAMF) is a proposed collection of formats and techniques to enable heterogeneous formal reasoning systems and users to communicate assertions in a decentralized, reliable, and egalitarian manner. An assertion is a unit of mathematical knowledge—think lemmas, theorems, corollaries, etc.—that is cryptographically signed by its originator.
DAMF is based on content-addressable storage using the InterPlanetary File System (IPFS) network, and uses the InterPlanetary Linked Data (IPLD) data model to represent assertions and all their components.
-
Functional Description:
Dispatch is an intermediary tool for publishing, retrieval, and trust analysis in the Distributed Assertion Management Framework (DAMF). Dispatch specifies a family of JSON-based formats for DAMF objects and implements the main DAMF processes. It is intended to be usable by both human users and tools.
Dispatch is being developed as part of the exploratory action W3Proof.
-
Release Contributions:
This initial version has a demonstration proof of a theorem using a combination of Coq, LambdaProlog, and Abella.
- URL:
- Publication:
-
Contact:
Kaustuv Chaudhuri
-
Participants:
Farah Al Wardani, Kaustuv Chaudhuri, Dale Miller
7.1.4 MOIN
-
Name:
MOdal Intuitionistic Nested sequents
-
Keywords:
Logic programming, Modal logic
-
Functional Description:
MOIN is a SWI Prolog theorem prover for classical and intuitionstic modal logics. The modal and intuitionistic modal logics considered are all the 15 systems occurring in the modal S5-cube, and all the decidable intuitionistic modal logics in the IS5-cube. MOIN also provides a protptype implementation for the intuitionistic logics for which decidability is not known (IK4,ID5 and IS4). MOIN is consists of a set of Prolog clauses, each clause representing a rule in one of the three proof systems. The clauses are recursively applied to a given formula, constructing a proof-search tree. The user selects the nested proof system, the logic, and the formula to be tested. In the case of classic nested sequent and Maehara-style nested sequents, MOIN yields a derivation, in case of success of the proof search, or a countermodel, in case of proof search failure. The countermodel for classical modal logics is a Kripke model, while for intuitionistic modal logic is a bi-relational model. In case of Gentzen-style nested sequents, the prover does not perform a countermodel extraction.
A system description of MOIN is available at https://hal.inria.fr/hal-02457240
- URL:
- Publication:
-
Contact:
Lutz Strassburger
-
Participants:
Lutz Strassburger, Marianna Girlando
7.1.5 Profound-Intuitionistic
-
Name:
Interactive theorem proving by direct manipulation for Intuitionistic Logic
-
Keywords:
Interactive Theorem Proving, First-order logic
-
Functional Description:
Profound-Intuitionistic (Profint) is a tool for building formal proofs in intuitionistic logic using an interactive direct manipulation based web-interface. The tool can transform the interactive proof into formal proof objects in a variety of backend provers including: Coq, Lean 3, Lean 4, Isabelle/HOL, HOL4, and Abella.
-
Release Contributions:
This release adds support for inductive theorem proving using sized relations in the style of Abella.
This release also adds preliminary support for three-dimensional representations of the proof state (using WebGL and the Three.js library).
- URL:
-
Contact:
Kaustuv Chaudhuri
7.1.6 YADE
-
Name:
Yet Another Diagram Editor
-
Keyword:
Diagram
-
Functional Description:
This diagram editor can help mechanising diagrammatic categorical proofs by generating Coq proof scripts from a drawn diagram. This is part of the Coreact ANR Project (started in March 2023), which aims at developing a methodology for diagrammatic reasoning in Coq.
- URL:
-
Contact:
Ambroise Lafont
-
Participant:
Ambroise Lafont
7.1.7 Coqlex
-
Keywords:
Coq, Lexical choice, Compilers
-
Functional Description:
Coqlex is a lexer generator for Coq. Users write a lexer in a custom DSL reminiscent of lex or ocamllex, and the tool produces Coq files that describe the lexer, provide a lexing function, and prove that the lexing function satisfies a declarative specification defined from the lexer description.
- URL:
- Publications:
-
Contact:
Lutz Strassburger
-
Participant:
4 anonymous participants
8 New results
8.1 Intuitionistic BV
Participants: Lutz Straßburger.
External Collaborators: Matteo Acclavio (Univ. of Sussex)
We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non- commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus. This work has been published in 12
8.2 A strictly linear subatomic proof system
Participants: Victoria Barrett.
External Collaborators: Benjamin Ralph (Univ. of Bath)
We present a subatomic deep-inference proof system for a conservative extension of propositional classical logic with decision trees that is strictly linear. In a strictly linear subatomic system, a single linear rule shape subsumes not only the structural rules, such as contraction and weakening, but also the unit equality rules. An interpretation map from subatomic logic to propositional classical logic recovers the usual semantics and proof theoretic properties. By using explicit substitutions that indicate the substitution of one derivation into another, we are able to show that the unit-equality inference steps can be eliminated from a subatomic system for propositional classical logic with only a polynomial complexity cost in the size of the derivation, from which it follows that the system p-simulates Frege systems, and we show cut elimination for the resulting strictly linear system. This work has been published in 13.
8.3 Proof Compression via Subatomic Logic and Guarded Substitutions
Participants: Lutz Straßburger, Victoria Barrett.
External Collaborators: Benjamin Ralph (Univ. of Bath)
Subatomic logic is a recent innovation in structural proof theory where atoms are no longer the smallest entity in a logical formula, but are instead treated as binary connectives. As a consequence, we can give a subatomic proof system for propositional classical logic such that all derivations are strictly linear: no inference step deletes or adds information, even units. In this paper, we introduce a powerful new proof compression mechanism that we call guarded substitutions, a variant of explicit substitutions, which substitute only guarded occurrences of a free variable, instead of all free occurrences. This allows us to construct "superpositions" of derivations, which simultaneously represent multiple subderivations. We show that a subatomic proof system with guarded substitution can p-simulate a Frege system with substitution, and moreover, the cut-rule is not required to do so. This is published in 14.
8.4 Designing a safe forward chaining tactic using productive proofs
Participants: Kaustuv Chaudhuri, Arunava Gantait, Dale Miller.
We present a proof-theoretic treatment of forward chaining and saturation within a multisorted, first-order intuitionistic logic with equality. The notions of polarity and focused proofs are central to our approach since they provide a characterization of geometric implications as bipolar formulas as well as a natural setting to describe forward chaining and the concept of productive proofs. We identify conditions under which forward chaining with a given set of formulas is guaranteed to saturate in a finite number of steps. The motivation for this research stems, in part, from exploring avenues to automate the Abella theorem prover, which relies on relational specifications, and where theorems in typical proof developments are essentially bipolar formulas. We illustrate the potential benefits of automating forward chaining and saturation for Abella by presenting examples that compute congruence closure and assist in other equational and relational reasoning tasks. This work has been published in 15.
8.5 Linear logic using negative connectives
Participants: Dale Miller.
In linear logic, the invertibility of a connective’s right-introduction rule is equivalent to the noninvertibility of its left-introduction rule. This duality motivates the concept of polarity: a connective is termed negative if its right-introduction rule is invertible, and positive otherwise. A two-sided sequent calculus for first-order linear logic featuring only negative connectives exhibits a compelling proof theory. Proof search in such a system unfolds through alternating phases of invertible (right-introduction) rules and non-invertible (left-introduction) rules, mirroring the processes ofgoal-reduction and backchaining, respectively. These phases are formalized here using the framework of multifocused proofs. We analyze linear logic by dissecting it into three sublogics: L0 (first-order intuitionistic logic with conjunction, implication, and universal quantification); L1 (an extension of L0 incorporating linear implication which preserves its intuitionistic nature); and L2 (which includes multiplicative falsity and encompasses classical linear logic). It is worth noting that the single-conclusion restriction on sequents, a constraint imposed by Gentzen, is not a prerequisite for defining intuitionistic logic proofs within this framework, as it emerges naturally by restricting the formulas to those of L0 and L1. While multifocused proofs of L2 sequents can accommodate parallel applications of left-introduction rules, proofs of L0 and L1 sequents cannot leverage such parallel rule applications. This notion of parallelism within proofs enables a novel approach to handling disjunctions and existential quantifiers in the natural deduction system for intuitionistic logic. This work has been published in 18
8.6 Asymptotic Distribution of Parameters in Trivalent Maps and Linear Lambda Terms
Participants: Noam Zeilberger.
External Collaborators: Olivier Bodini (Université Paris Nord), Alexandros Singh (Université Paris 8)
In this work, we study the limit distributions of various combinatorial parameters in trivalent maps, linear -terms, and other related families of objects. We focus on parameters in maps which naturally correspond to parameters in -terms and vice versa, allowing us to employ techniques from map theory and the -calculus in a combinatorial interplay. Some examples of the parameters we study are: the number of bridges in rooted trivalent maps and of subterms in closed linear -terms as well as the number of vertices of degree 1 in -valent maps and of free variables in open linear -terms. To analyse their distributions, we introduce appropriate tools: a moment-pumping schema for differential equations and a composition schema inspired by Bender's theorem.
This work has been published in the diamond open access journal Combinatorial Theory 6.
8.7 The categorical contours of the Chomsky-Schützenberger representation theorem
Participants: Noam Zeilberger.
External Collaborators: Paul-André Melliès (Université Paris Cité, CNRS, Inria)
We develop fibrational perspectives on context-free grammars and on nondeterministic finite-state automata over categories and operads. A generalized CFG is a functor from a free colored operad (aka multicategory) generated by a pointed finite species into an arbitrary base operad: this encompasses classical CFGs by taking the base to be a certain operad constructed from a free monoid, as an instance of a more general construction of an operad of spliced arrows for any category . A generalized NFA is a functor from an arbitrary bipointed category or pointed operad satisfying the unique lifting of factorizations and finite fiber properties: this encompasses classical word automata and tree automata without -transitions, but also automata over non-free categories and operads. We show that generalized context-free and regular languages satisfy suitable generalizations of many of the usual closure properties, and in particular we give a simple conceptual proof that context-free languages are closed under intersection with regular languages. Finally, we observe that the splicing functor admits a left adjoint , which we call the contour category construction since the arrows of have a geometric interpretation as oriented contours of operations of . A direct consequence of the contour / splicing adjunction is that every pointed finite species induces a universal CFG generating a language of tree contour words. This leads us to a generalization of the Chomsky-Schützenberger Representation Theorem, establishing that a subset of a homset is a CFL of arrows if and only if it is a functorial image of the intersection of a -chromatic tree contour language with a regular language.
This work has been published in the diamond open access journal Logical Methods in Computer Science 7.
8.8 The free bifibration over a functor
Participants: Noam Zeilberger.
External Collaborators: Bryce Clarke (Tallinn University of Technology, Estonia), Gabriel Scherer (Inria, IRIF)
We consider the problem of constructing the free bifibration generated by a functor . This problem was previously considered by Lamarche, and is closely related to the problem, considered by Dawson, Paré, and Pronk, of “freely adjoining adjoints” to a category. We develop a proof-theoretic approach to the problem, beginning with a construction of the free bifibration in which objects of are formulas of a primitive “bifibrational logic”, and arrows are derivations in a cut-free sequent calculus modulo a notion of permutation equivalence. We show that instantiating the construction to the identity functor generates a zigzag double category, which is also the free double category with companions and conjoints (or fibrant double category) on . The approach adapts smoothly to the more general task of building -fibrations, where one only asks for pushforwards along arrows in and pullbacks along arrows in for some subsets of arrows, which encompasses Kock and Joyal's notion of ambifibration when form a factorization system. We establish a series of progressively stronger normal forms, guided by ideas of focusing from proof theory, and obtain a canonicity result under assumption that the base category is factorization preordered relative to and . This canonicity result allows us to decide the word problem and to enumerate relative homsets without duplicates. Finally, we describe several examples of a combinatorial nature, including a category of plane trees generated as a free bifibration over , and a category of increasing forests generated as a free ambifibration over , which contains the lattices of noncrossing partitions as quotients of its fibers by the Beck-Chevalley condition.
This work has been published as a 95-page preprint 22 and submitted to the diamond open access journal Higher Structures.
8.9 Interaction Equivalence
Participants: Beniamino Accattoli, Adrienne Lancelot.
External Collaborators: Giulio Manzonetto (IRIF, Université Paris Cité), Garbiele Vanoni (IRIF, Université Paris Cité).
Contextual equivalence is the de facto standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does not induce an equational theory, for an apparently essential reason: cost is not invariant under reduction.
In the paradigmatic case of the untyped -calculus, we introduce interaction equivalence. Inspired by game semantics, we observe the number of interaction steps between terms and contexts but—crucially—ignore their internal steps. We prove that interaction equivalence is an equational theory and characterize it as , the well-known theory induced by Böhm tree equality. It is the first observational characterization of obtained without enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the Böhm-out technique and of intersection types.
This work was published in the proceeding of POPL 2025 3, one of the flagship conferences of he field.
8.10 Barendregt’s Theory of the -Calculus, Refreshed and Formalized
Participants: Beniamino Accattoli, Adrienne Lancelot.
External Collaborators: Maxime Vemclefs (independent researcher).
Barendregt's book on the untyped -calculus refines the inconsistent view of -divergence as representation of the undefined via the key concept of head reduction.
In this paper, we put together recent revisitations of some key theorems laid out in Barendregt's book, and we formalize them in the Abella proof assistant. Our work provides a compact and refreshed presentation of the core of the book.
The formalization faithfully mimics pen-and-paper proofs. Two interesting aspects are the manipulation of contexts for the study of contextual equivalence and a formal alternative to the informal trick at work in Takahashi's proof of the genericity lemma. As a by-product, we obtain an alternative definition of contextual equivalence that does not mention contexts.
This work was published in the international conference ITP 2025 16.
8.11 The Cost of Skeletal Call-By-Need, Smoothly
Participants: Beniamino Accattoli.
External Collaborators: Francesco Magliocca (University of Naples Federico II), Loïc Payrot (IMDEA), Claudio Sacerdoti Coen (University of Bologna).
Skeletal call-by-need is an optimization of call-by-need evaluation also known as “fully lazy sharing”: when the duplication of a value has to take place, it is first split into “skeleton”, which is then duplicated, and “flesh” which is instead kept shared.
Here, we provide two cost analyses of skeletal call-by-need. Firstly, we provide a family of terms showing that skeletal call-by-need can be asymptotically exponentially faster than call-by-need in both time and space; it is the first such evidence, to our knowledge.
Secondly, we prove that skeletal call-by-need can be implemented efficiently, that is, with bi-linear overhead. This result is obtained by providing a new smooth presentation of ideas by Shivers and Wand for the reconstruction of skeletons, which is then smoothly plugged into the study of an abstract machine following the distillation technique by Accattoli et al.
This work was published in the international conference FSCD 2025 9.
8.12 The Vanilla Sequent Calculus is Call-by-Value
Participants: Beniamino Accattoli.
Existing Curry-Howard interpretations of call-by-value evaluation for the -calculus are either based on ad-hoc modifications of intuitionistic proof systems or involve additional logical concepts such as classical logic or linear logic, despite the fact that call-by-value was introduced in an intuitionistic setting without linear features.
This paper shows that the most basic sequent calculus for minimal intuitionistic logic—dubbed here vanilla—can naturally be seen as a logical interpretation of call-by-value evaluation. This is obtained by establishing mutual simulations with a well-known formalism for call-by-value evaluation.
This work was published in the international conference ESOP 2025 11.
8.13 Positive Sharing and Abstract Machines
Participants: Beniamino Accattoli.
External Collaborators: Claudio Sacerdoti Coen (University of Bologna), Jui-Hsuan Wu (LIP, ENS de Lyon).
Wu's positive -calculus is a recent call-by-value -calculus with sharing coming from Miller and Wu's study of the proof-theoretical concept of focalization. Accattoli and Wu showed that it simplifies a technical aspect of the study of sharing; namely it rules out the recurrent issue of renaming chains, that often causes a quadratic time slowdown.
In this paper, we define the natural abstract machine for the positive -calculus and show that it suffers from an inefficiency: the quadratic slowdown somehow reappears when analyzing the cost of the machine. We then design an optimized machine for the positive -calculus, which we prove efficient. The optimization is based on a new slicing technique which is dual to the standard structure of machine environments.
This work was published in the international conference APLAS 2025 10, and received the best paper award of the conference.
8.14 Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
Participants: Beniamino Accattoli.
External Collaborators: Cláudio Belo Lourenço (Huawei), Dan R. Ghica (University of Birmingham & Huawei), Giulio Guerrieri (University of Sussex), Claudio Sacerdoti Coen (University of Bologna), Jui-Hsuan Wu (LIP, ENS de Lyon).
Closure conversion is a program transformation at work in compilers for functional languages to turn inner functions into global ones, by building closures pairing the transformed functions with the environment of their free variables. Abstract machines rely on similar and yet different concepts of closures and environments. We study the relationship between the two approaches. We adopt a simple lambda-calculus with tuples as source language and study abstract machines for both the source language and the target of closure conversion. Moreover, we focus on the simple case of flat closures/environments (no sharing of environments).
We provide three contributions. Firstly, a new simple proof technique for the correctness of closure conversion, inspired by abstract machines. Secondly, we show how the closure invariants of the target language allow us to design a new way of handling environments in abstract machines, not su!ering the shortcomings of other styles. Thirdly, we study the machines from the point of view of time complexity. We show that closure conversion decreases various dynamic costs while increasing the size of the initial code. Despite these changes, the overall complexity of the machines before and after closure conversion turns out to be the same.
This work was published in the international conference PPDP 2025 8.
8.15 Separating Terms by Means of Multi Types, Coinductively
Participants: Adrienne Lancelot.
Intersection type systems, as adequate models of the λ-calculus, induce an equational theory on terms,that we refer to as type equivalence. We give a new proof technique to coinductively characterize type equivalence. To do so, we explore a simple setting, namely weak head type equivalence, which is the equational theory induced by a weak head non-idempotent intersection type system.
We prove a folklore result: weak head type equivalence coincides with Sangiorgi’s normal form bisimilarity. What is new in our development is that we only rely on coinductive program equivalences, bypassing the need to introduce term approximants, which were used in previous works characterizing type equivalence.
The crucial part of this characterization is to show that type equivalent terms are normal form bisimilar: we do so by constructing shape typings that can only type terms of a specific normal form structure. Shape typings are a light form of principal types, a technique often used in intersection types to generate from one or few principal typing all possible typings of a term.
This work was published in the post-proceedings of the international conference TYPES 2024 (which were published in 2025) 17.
8.16 2-Functoriality of Initial Semantics
Participants: Ambroise Lafont.
External Collaborators: Thomas Lamiaux (INRIA, Gallinette), Benedikt Ahrens (TU Delft)
Initial semantics aims to model inductive structures and their properties, and to provide them with recursion principles respecting these properties. An ubiquitous example is the fold operator for lists. We are concerned with initial semantics that model languages with variable binding and their substitution structure, and that provide substitution-safe recursion principles. There are different approaches to implementing languages with variable binding depending on the choice of representation for contexts and free variables, such as unscoped syntax, or well-scoped syntax with finite or infinite contexts. Abstractly, each approach corresponds to choosing a different monoidal category to model contexts and binding, each choice yielding a different notion of "model" for the same abstract specification (or "signature"). In this work, we provide tools to compare and relate the models obtained from a signature for different choices of monoidal category. We do so by showing that initial semantics naturally has a 2-categorical structure when parametrized by the monoidal category modeling contexts. We thus can relate models obtained from different choices of monoidal categories provided the monoidal categories themselves are related. In particular, we use our results to relate the models of the different implementation - de Bruijn vs locally nameless, finite vs infinite contexts -, and to provide a generalized recursion principle for simply-typed syntax.
This work was published in the international conference ICFP 2025 4.
8.17 From Semantics to Syntax: A Type Theory for Comprehension Categories
Participants: Niyousha Najmaei.
External Collaborators: Niels van der Weide, Benedikt Ahrens, Paige Randall North
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.
This work was published in the international conference POPL 2026 23.
9 Partnerships and cooperations
9.1 International initiatives
9.1.1 STIC/MATH/CLIMAT AmSud projects
DLR
-
Title:
Dynamic logics (reloaded)
-
Program:
STIC-AmSud
-
Duration:
January 1, 2024 – December 31, 2025
-
Local supervisor:
Lutz Strassburger
-
Partners:
- Carlos Areces, Facultad de Matemática, Astronomía, Física y Computación, Universidad Nacional de Córdoba (Argentine)
- Mario R. F. Benevides, Instituto de Computação, Universidade Federal Fluminense (Brésil)
- Pablo Barceló, Institute for Mathematical and Computational Engineering, Universidad Católica de Chile y Millennium Institute for Foundational Research on Data (Chili)
- Stéphane Demri, LMF (France)
-
Inria contact:
Lutz Strassburger
-
Summary:
During the project we will advance our understanding of a novel family of logics called dynamic logics. Dynamic logics are characterized by the inclusion of operators that can modify the model in which they are being evaluated. This characteristic made them especially well suited for the description of evolving scenarios like, for example, the temporal evolution of a communication network, where connections are dynamically created and eliminated, constantly changing the actual topology. A number of different dynamic logics have been investigated (see [AB10, MFBMM11, BM11, AFM12, DD14, MS14, AFH15, BM17, ABFF18, DF18, DFM19] among others) by members of the project, but a general perspective is still missing, and a number of important open questions remains, ranging from adequate model theoretic characterizations, to a proper understanding of how to define proof calculi for these logics. In recent years, the potential applications of dynamic logics have grown, with the recent rise of AI techniques based on knowledge represented as large graphs. The project aims to pull together the strengths of the five international research teams, to unify existing results and attempt to answer these open problems.
9.1.2 Participation in other International Programs
PHC Sophie Germain
-
Title:
Formal Verification for Large Language Models
-
Coordinator:
Lutz Strassburger
-
Partner Institution:
UCL, UK
-
Date/Duration:
01/01/2025 – 31/12/2025
-
Summary:
Methods from proof theory and formal verification can significantly enhance the reliability and trustworthiness of Large Language Models (LLMs). By applying formal verification, we can systematically ensure that LLMs adhere to specified properties and constraints, addressing several key challenges in their deployment.
9.2 National initiatives
LambdaComb
-
Title:
LambdaComb: a cartographic quest between lambda-calculus, logic, and combinatorics
-
Duration:
2022 – 2026 (4 years)
-
Coordinator:
Noam Zeilberger
-
Partners:
- LIX (Ecole Polytechnique), LIPN (Paris Nord), LIS (Marseille), LIGM (Marne-la-Vallée)
- Jagiellonian University (Poland)
-
Summary:
LambdaComb is an interdisciplinary project financed by the Agence Nationale de la Recherche (PRC grant ANR-21-CE48-0017). Broadly, the project aims to deepen connections between lambda calculus and logic on the one hand and combinatorics on the other. One important motivation for the project is the discovery over recent years of a host of surprising links between subsystems of lambda calculus and enumeration of graphs on surfaces, or "maps", the latter being an active subfield of combinatorics with roots in W. T. Tutte's work in the 1960s. Using these new links and other ideas and tools, the LambdaComb project aims to:
- develop rigorous logical perspectives on maps and related combinatorial objects; and
- develop precise quantitative perspectives on lambda calculus and related systems.
The project also intersects with and aims to shed new light on other established connections between logic and geometry, notably Joyal and Street's categorical framework of string diagrams as well as Girard's proof nets for linear logic.
CoREACT
-
Title:
CoREACT: Coq-based Rewriting: towards Executable Applied Category Theory
-
Duration:
2023 – 2027 (4 years)
-
Coordinator:
Nicolas Behr
-
Partners:
IRIF (Université Paris Cité), LIP (ENS-Lyon), LIX (Ecole Polytechnique), Sophia-Antipolis (Inria)
-
Local participants:
Ambroise Lafont , Benjamin Werner , Noam Zeilberger
-
Summary:
The main objectives of the CoREACT project include:
- Development of a methodology for diagrammatic reasoning in Coq
- Formalization and certification of a representative collection of axioms and theorems for compositional categorical rewriting theory
- Development of a Coq-enabled interactive database and wiki system
- Development of a CoREACT wiki-based "proof-by-pointing" engine
- Executable reference prototype algorithms from categorical structures in Coq (via the use of SMT solvers/theorem provers such as Z3)
10 Dissemination
10.1 Promoting scientific activities
Member of the organizing committees
- Miller has been on the Steering Committee of LICS (Logic in Computer Science) since 2012.
- Zeilberger organized the Journées LambdaComb workshop at CIRM, within the context of the ANR LambdaComb project which is nearing the end of its official lifetime.
- Strassburger was coorganizer of the BIRS seminar 25w5406 “Proof Representations: From Theory to Applications” in Banff, Canada, June 1–6, 2025
10.1.1 Scientific events: selection
- Miller has been a member of ACM’s Heidelberg Laureate Forum Young Researcher Selection Committee since 2024.
- Miller has been a proposal reviewer for Research Foundation of Flanders (FWO) and Deutsche Forschungsgemeinschaft (DFG).
Member of the conference program committees
- Chaudhuri was a PC co-chair for LFMTP 2025
- Miller has been a member of the program committees for CSL 2025 (33rd Annual Conference of the European Association for Computer Science Logic) and HCVS 2025 (the 12th International Workshop on Horn Clauses for Verification and Synthesis).
- Accattoli was a member of the program committee for LSFA 2025 (the 20th International Symposium on Logical and Semantic Frameworks, with Applications).
- Lafont was a member of the program committee for POPL 2026 (the 53rd ACM SIGPLAN Symposium on Principles of Programming Languages).
Reviewer:
- Strassburger was a reviewer for MFCS 2025,FSCD 2025, and LICS 2025.
- Accattoli was a reviewer for FoSSaCS 2026 and CSL 2026.
- Lafont was a reviewer for CPP 2026, LICS 2025 and FSCD 2025.
- Miller was a reviewer for LICS 2025 and FSCD 2025.
10.1.2 Journal:
Member of the editorial boards
- Miller has been a member of Editorial Board of the Journal of Automated Reasoning (published by Springer) since May 2011.
- Miller is a guest co-editor for a special issue of papers selected from FLOPS 2024 for the Science of Computer Programming.
Reviewer - reviewing activities
- Zeilberger was a reviewer for Theory and Applications of Categories and Compositionality.
- Strassburger was a reviewer for Annals of Pure and Applied Logic.
- Accattoli was a reviewer for the Journal on Functional Programming.
- Miller was a reviewer for Studia Logica, Journal of Logic and Computation, Journal of Symbolic Logic, Bulletin of the Section of Logic, and Oxford University Press.
10.1.3 Invited talks
- Dale Miller was an invited speaker at TLLA 2025 (Trends in Linear Logic and Applications), the Special session on proof theory during Logic Colloquium 2025, and the Workshop on “Proof Representations: From Theory to Applications” in Banff, Canada.
- Noam Zeilberger gave an invited tutorial at the Dagstuhl Seminar on Categories for Automata and Language Theory (March 30 - April 4).
- Chaudhuri was a joint invited speaker at TABLEAUX 2025 and FroCoS 2025 in Reykjavík, Iceland.
- Accattoli was an invited speaker at the Workshop on Reasoning with Quantitative Types, held in Porto on June 5-6, 2025, Portugal.
10.1.4 Scientific expertise
- Strassburger wrote a book review for Oxford University Press
10.1.5 Research administration
- Strassburger is member of the BCEP at Inria Saclay.
- Accattoli is a member of the commission scientifique at Inria Saclay.
10.2 Teaching - Supervision - Juries - Educational and pedagogical outreach
10.2.1 University-level teaching
- Werner is in charge of the course "Foundations of Proof Systems" in the joint MPRI Master program (28 hours). He is in charge of the course "Mécanismes d'un langage de programmation orienté-objet" in the cycle ingénieur polytechnicien (10 weeks, 250 students) and of the course "Logic and Proofs" of the BSc program of Ecole polytechnique (16 weeks, 60 students).
- Lafont taught 90 hours in the Bachelors program of Ecole Polytechnique for the following courses: Introduction to algorithms, Logic and proofs, Concurrent and Distributed Computing, Introduction to Formal Languages.
- Zeilberger taught 128 hours in the Bachelors and Polytechniciens programs of Ecole Polytechnique for the following courses: Computer Programming, Introduction to Formal Languages, Functional Programming, Fondements de l'informatique.
- Strassburger and Barrett have been teaching a course at ESSLLI2025 in Bochum (August 2025)
10.2.2 Supervision
- Kaustuv Chaudhuri and Dale Miller were the PhD co-advisors of Farah Al Wardani and Arunava Gantait.
- Accattoli supervised the PhD student Adrienne Lancelot, who defended her thesis on the 13th of November 2025.
- Ambroise Lafont and Benjamin Werner were the PhD co-advisors of Niyousha Najmaei.
10.2.3 Juries
- Miller was on the PhD jury for Emilie Grienenberger, University of Paris-Saclay, 3 February 2025
- Zeilberger served as opponent at the PhD defense of Matthew Earnshaw (Tallinn University of Technology) in January, and as external examiner at the PhD defense of Malin Altenmüller (Strathclyde University) in December (both positions being roughly equivalent to the French rapporteur).
- Strassburger served as external examiner at the PhD defense of William Simmons, University of Oxford, January 7, 2025
- Lafont was in the jury of Luc Chabassier, who defended his PhD on the 7th of July 2025.
10.2.4 Educational and pedagogical outreach
- Werner has initiated discussions with the Mathematics teachers of the Lycée International de Palaiseau, to explore the possibility to use novel formal proof interfaces in education.
10.3 Popularization
10.3.1 Specific official responsibilities in science outreach structures
- Chaudhuri is a volunteer moderator for CoRR and arXiv in the cs.LO category
11 Scientific production
11.1 Major publications
- 1 articleInteraction Equivalence.Proceedings of the ACM on Programming Languages9POPLJanuary 2025, 1627-1656HALDOI
- 2 inproceedingsProof Compression via Subatomic Logic and Guarded Substitutions.LICS 2025 - 40th Annual ACM/IEEE Symposium on Logic in Computer ScienceSingapore, SingaporeIEEEMay 2025, 183-195HALDOI
11.2 Publications of the year
International journals
International peer-reviewed conferences
Scientific books
Doctoral dissertations and habilitation theses
Reports & preprints