66 Search Results for "Forster, Yannick"

Volume

LIPIcs, Volume 352

16th International Conference on Interactive Theorem Proving (ITP 2025)

ITP 2025, September 28 to October 1, 2025, Reykjavik, Iceland

Editors: Yannick Forster and Chantal Keller

Document
DOI: 10.4230/LIPIcs.TYPES.2025.2
Lean4Lean: Verifying a Typechecker for Lean, in Lean

Authors: Mario Carneiro

Published in: LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025)

Abstract
In this paper we present a new "external checker" for the Lean theorem prover, written in Lean itself. This is the first complete typechecker for Lean 4 other than the reference implementation in C++ used by Lean itself, and our new checker is competitive with the original, running between 20% and 50% slower and usable to verify all of Lean’s Mathlib library, taking an additional step in Lean’s aim to self-host the full elaborator and compiler. Moreover, because the checker is written in a language which admits formal verification, it is possible to state and prove properties about the kernel itself, and we report on progress to formalize the Lean type theory abstractly and prove some theorems about it. Finally, we combine these to get a proof of correctness of parts of the kernel. We plan to use this project to help justify any future changes to the kernel and type theory and ensure unsoundness does not sneak in through either the abstract theory or implementation bugs. The verification is already paying off, as one soundness bug has been spotted and fixed as a result of this work.
Cite as

Mario Carneiro. Lean4Lean: Verifying a Typechecker for Lean, in Lean. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{carneiro:LIPIcs.TYPES.2025.2,
  author =	{Carneiro, Mario},
  title =	{{Lean4Lean: Verifying a Typechecker for Lean, in Lean}},
  booktitle =	{31st International Conference on Types for Proofs and Programs (TYPES 2025)},
  pages =	{2:1--2:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-441-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{384},
  editor =	{Nordvall Forsberg, Fredrik and McKinna, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.2},
  URN =		{urn:nbn:de:0030-drops-270206},
  doi =		{10.4230/LIPIcs.TYPES.2025.2},
  annote =	{Keywords: Lean, proof assistant, external typechecker, implementation, metatheory, type theory, proof theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2026.5
Not Choosing Is Still a Choice: Constructive mathematics without any choice

Authors: Martin Baillon, Yannick Forster, Dominik Kirst, Assia Mahboubi, and Pierre-Marie Pédrot

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract
The axiom of choice (AC) states that every total relation contains a function. It enjoys a pivotal role in both classical and constructive dialects of mathematics. In the former, it is seen as a useful closure property invoked especially in set-theoretic contexts, in the latter it is seen either as a tautology, following from a constructive reading of totality proofs, or as a taboo, as by an extensional reading of totality proofs it enforces full classical logic. It has therefore been debated how much of AC should be accepted in constructive foundations and authors like Richman argued for "Constructive mathematics without choice" where even countable choice, not immediately jeopardising constructive reasoning, is avoided. With this paper, we propose a continuation of Richman’s programme of more radical extent and systematically study constructive foundations absent of countable, unique, or quantifier-free choice principles as well as the spurious fragments of (the actual) AC in form of extensionality principles: "Constructive mathematics without any choice" We argue that such a minimalistic setting is advantageous, for instance for studies in constructive reverse mathematics and synthetic computability theory. Apart from these programmatic considerations and a careful encyclopedia of choice principles, we revisit and refine several results from the literature: We show that already the partition principle (a consequence of AC of unknown strength) implies the excluded middle, that already logically decidable (inductive) equality of propositions implies proof irrelevance, and that function inversion principles such as the Cantor-Bernstein theorem not only rely on the excluded middle but also on unique choice. To the best of our knowledge, the latter is the first reverse mathematics result regarding the full axiom of unique choice, enabled by our minimal setting. Implementing such a minimalistic foundation, the proofs of all our results have been mechanised with the Rocq prover.
Cite as

Martin Baillon, Yannick Forster, Dominik Kirst, Assia Mahboubi, and Pierre-Marie Pédrot. Not Choosing Is Still a Choice: Constructive mathematics without any choice. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{baillon_et_al:LIPIcs.FSCD.2026.5,
  author =	{Baillon, Martin and Forster, Yannick and Kirst, Dominik and Mahboubi, Assia and P\'{e}drot, Pierre-Marie},
  title =	{{Not Choosing Is Still a Choice: Constructive mathematics without any choice}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{5:1--5:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.5},
  URN =		{urn:nbn:de:0030-drops-263553},
  doi =		{10.4230/LIPIcs.FSCD.2026.5},
  annote =	{Keywords: Axiom of Choice, Constructive Mathematics, Type Theory}
}
Document
Invited Paper
DOI: 10.4230/OASIcs.RW.2024/2025.7
Modern Datalog: Concepts, Methods, Applications (Invited Paper)

Authors: Markus Krötzsch

Published in: OASIcs, Volume 138, Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025)

Abstract
Pure Datalog is arguably the most fundamental rule language, elegant and simple, but also often too limited to be useful in practice. This has motivated the introduction of many new expressive features, ranging from datatypes and related functions, over aggregates and semi-ring generalisations, to existential quantifiers and complex terms. In spite of their variety, all these approaches remain true to the nature of Datalog as a direct, pattern-based way of computing on structured data. We therefore find that a modern notion of Datalog is emerging, distinctly different from other approaches of logic programming and with its own set of related methods and applications. In this course, we introduce Datalog and its most common extensions, and explain when and how these features can be used together (which is often, but not always, safe to do). We further look at modern Datalog systems and some of their primary use cases. Hands-on work with Datalog and its extensions is done with the free Datalog engine https://knowsys.github.io/nemo-doc/. The course is accessible to all audiences and does not assume specific prior knowledge.
Cite as

Markus Krötzsch. Modern Datalog: Concepts, Methods, Applications (Invited Paper). In Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025). Open Access Series in Informatics (OASIcs), Volume 138, pp. 7:1-7:41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{krotzsch:OASIcs.RW.2024/2025.7,
  author =	{Kr\"{o}tzsch, Markus},
  title =	{{Modern Datalog: Concepts, Methods, Applications}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{7:1--7:41},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-405-5},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{138},
  editor =	{Artale, Alessandro and Bienvenu, Meghyn and Garc{\'\i}a, Yazm{\'\i}n Ib\'{a}\~{n}ez and Murlak, Filip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.RW.2024/2025.7},
  URN =		{urn:nbn:de:0030-drops-250524},
  doi =		{10.4230/OASIcs.RW.2024/2025.7},
  annote =	{Keywords: Datalog, query language, knowlegde representation and reasoning, logic programming, Horn logic, SPARQL, datatypes and aggregation, lecture notes, tutorial}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.ITP.2025
LIPIcs, Volume 352, ITP 2025, Complete Volume

Authors: Yannick Forster and Chantal Keller

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
LIPIcs, Volume 352, ITP 2025, Complete Volume
Cite as

16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 1-764, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Proceedings{forster_et_al:LIPIcs.ITP.2025,
  title =	{{LIPIcs, Volume 352, ITP 2025, Complete Volume}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{1--764},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025},
  URN =		{urn:nbn:de:0030-drops-247775},
  doi =		{10.4230/LIPIcs.ITP.2025},
  annote =	{Keywords: LIPIcs, Volume 352, ITP 2025, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ITP.2025.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Yannick Forster and Chantal Keller

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.ITP.2025.0,
  author =	{Forster, Yannick and Keller, Chantal},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{0:i--0:xviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.0},
  URN =		{urn:nbn:de:0030-drops-247752},
  doi =		{10.4230/LIPIcs.ITP.2025.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.17
Formalising Inductive and Coinductive Containers

Authors: Stefania Damato, Thorsten Altenkirch, and Axel Ljungström

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of locally cartesian closed categories (LCCCs) with disjoint coproducts and W-types, and uniqueness of identity proofs (UIP) is implicitly assumed throughout. Although it is claimed that these developments can also be interpreted in extensional Martin-Löf type theory, this interpretation is not made explicit. In this paper, we present a formalisation of the results that "containers preserve least and greatest fixed points" in Cubical Agda, thereby giving a formulation in intensional type theory. Our proofs do not make use of UIP and thereby generalise the original results from talking about container functors on Set to container functors on the wild category of types. Our main incentive for using Cubical Agda is that its path type restores the equivalence between bisimulation and coinductive equality. Thus, besides developing container theory in a more general setting, we also demonstrate the usefulness of Cubical Agda’s path type to coinductive proofs.
Cite as

Stefania Damato, Thorsten Altenkirch, and Axel Ljungström. Formalising Inductive and Coinductive Containers. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{damato_et_al:LIPIcs.ITP.2025.17,
  author =	{Damato, Stefania and Altenkirch, Thorsten and Ljungstr\"{o}m, Axel},
  title =	{{Formalising Inductive and Coinductive Containers}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.17},
  URN =		{urn:nbn:de:0030-drops-246151},
  doi =		{10.4230/LIPIcs.ITP.2025.17},
  annote =	{Keywords: type theory, container, initial algebra, terminal coalgebra, Cubical Agda}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.19
Formalising Subject Reduction and Progress for Multiparty Session Processes

Authors: Burak Ekici, Tadayoshi Kamegai, and Nobuko Yoshida

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Multiparty session types (MPST) provide a robust typing discipline for specifying and verifying communication protocols in concurrent and distributed systems involving multiple participants. This work formalises the non-stuck theorem for synchronous MPST in the Coq proof assistant, ensuring that well-typed communications never get stuck. We present a fully mechanised proof of the theorem, where recursive type unfoldings are modelled as infinite trees, leveraging coinductive reasoning. This marks the first formal proof to incorporate precise subtyping, aiming to extend the typability of processes thus precision of the type system. The proof is grounded in fundamental properties such as subject reduction and progress. During the mechanisation process, we discovered that the structural congruence rule for recursive processes, as presented in several prior works on MPST, violates subject reduction. We resolve this issue by revising and formalising the rule to ensure the preservation of type soundness. Our approach to formal proofs about infinite type trees involves analysing their finite prefixes through inductive reasoning within outer-level coinductively stated goals. We employ the greatest fixed point of the parameterised least fixed point technique to define coinductive predicates and use parameterised coinduction to prove properties. The formalisation comprises approximately 16K lines of Coq code, accessible at: https://github.com/Apiros3/smpst-sr-smer.
Cite as

Burak Ekici, Tadayoshi Kamegai, and Nobuko Yoshida. Formalising Subject Reduction and Progress for Multiparty Session Processes. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ekici_et_al:LIPIcs.ITP.2025.19,
  author =	{Ekici, Burak and Kamegai, Tadayoshi and Yoshida, Nobuko},
  title =	{{Formalising Subject Reduction and Progress for Multiparty Session Processes}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{19:1--19:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.19},
  URN =		{urn:nbn:de:0030-drops-246177},
  doi =		{10.4230/LIPIcs.ITP.2025.19},
  annote =	{Keywords: multiparty session types, type trees, subtyping, progress, subject reduction, non-stuck theorem, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.21
Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation

Authors: Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, and Takafumi Saikawa

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Concentration inequalities are standard lemmas providing upper bounds on deviations of random variables. To formalize concentration inequalities, we have been developing a general library of lemmas for probability theory in the Rocq prover. This effort led us to revisit already established technical aspects of the Mathematical Components libraries. In this paper, we report on improvements of general interest resulting from our formalization. We devise types for numeric values and a lightweight semi-decision procedure, based on interval arithmetic. We also extend the hierarchy of available mathematical structures to formalize Lebesgue spaces. We illustrate our new formalization of probability theory with the complete proof of a concentration inequality for Bernoulli sampling.
Cite as

Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, and Takafumi Saikawa. Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.ITP.2025.21,
  author =	{Affeldt, Reynald and Bruni, Alessandro and Cohen, Cyril and Roux, Pierre and Saikawa, Takafumi},
  title =	{{Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{21:1--21:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.21},
  URN =		{urn:nbn:de:0030-drops-246195},
  doi =		{10.4230/LIPIcs.ITP.2025.21},
  annote =	{Keywords: Rocq prover, Mathematical Components library, abstraction interpretation, probability theory, concentration inequalities}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.25
GOL in GOL in HOL: Verified Circuits in Conway’s Game of Life

Authors: Magnus O. Myreen and Mario Carneiro

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Conway’s Game of Life (GOL) is a cellular automaton that has captured the interest of hobbyists and mathematicians alike for more than 50 years. The Game of Life is Turing complete, and people have been building increasingly sophisticated constructions within GOL, such as 8-bit displays, Turing machines, and even an implementation of GOL itself. In this paper, we report on a project to build an implementation of GOL within GOL, via logic circuits, fully formally verified within the HOL4 theorem prover. This required a combination of interactive tactic proving, symbolic simulation, and semi-automated forward proof to assemble the components into an infinite circuit which can calculate the next step of the simulation while respecting signal propagation delays. The result is a verified "GOL in GOL compiler" which takes an initial GOL state and returns a mega-cell version of it that can be passed to off-the-shelf GOL simulators, such as Golly. We believe these techniques are also applicable to other cellular automata, as well as for hardware verification which takes into account both the physical configuration of components and wire delays.
Cite as

Magnus O. Myreen and Mario Carneiro. GOL in GOL in HOL: Verified Circuits in Conway’s Game of Life. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{myreen_et_al:LIPIcs.ITP.2025.25,
  author =	{Myreen, Magnus O. and Carneiro, Mario},
  title =	{{GOL in GOL in HOL: Verified Circuits in Conway’s Game of Life}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.25},
  URN =		{urn:nbn:de:0030-drops-246230},
  doi =		{10.4230/LIPIcs.ITP.2025.25},
  annote =	{Keywords: Cellular automata, Higher-order logic, Interactive theorem proving}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.27
Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic

Authors: Robbert Krebbers, Luko van der Maas, and Enrico Tassi

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Inductive predicates play a key role in program verification using separation logic. There are many methods for defining such predicates in separation logic, which all have different conditions and thus support different classes of predicates. The most common methods are: (1) through a structurally-recursive definition (commonly used to define representation predicates for the verification of data structures), and (2) through step-indexing (commonly used to give a semantics of Hoare triples for partial program correctness). A lesser-known method is to define such inductive predicates internally in higher-order separation logic through a least fixpoint of a monotone function. The contributions of this paper are fourfold. First, we present the folklore result (from the Iris library) that one can define least (and greatest) fixpoints internally in separation logic by extending the standard second-order impredicative encoding with some modalities. Second, we show that these fixpoints are useful to define representation predicates where the mathematical and in-memory data structures do not correspond. Third, we show that these fixpoints can be used to define Hoare triples and weakest preconditions for total program correctness in Iris. Fourth, we present a prototype command (akin to Rocq’s Inductive), written in Rocq-Elpi, to generate the least fixpoint and its reasoning principles (constructors and induction principles) from a high-level specification.
Cite as

Robbert Krebbers, Luko van der Maas, and Enrico Tassi. Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 27:1-27:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{krebbers_et_al:LIPIcs.ITP.2025.27,
  author =	{Krebbers, Robbert and van der Maas, Luko and Tassi, Enrico},
  title =	{{Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{27:1--27:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.27},
  URN =		{urn:nbn:de:0030-drops-246258},
  doi =		{10.4230/LIPIcs.ITP.2025.27},
  annote =	{Keywords: Separation Logic, Program Verification, Data Structures, Iris, Rocq prover}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.28
Mechanising Böhm Trees and λη-Completeness

Authors: Chun Tian and Michael Norrish

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The Böhm tree is a critical notion in untyped λ-calculus, capturing the semantics of β-reduction. It underpins the proof that the equational theory of βη-equivalence is Hilbert-Post complete. This paper presents the first formalisation of this result, following the classic text by Barendregt. It includes a coinductive definition of Böhm trees, and then uses the "Böhm out" technique to prove a restricted version of Böhm’s separability theorem, which leads to the completeness theorem. Carrying out the proofs in HOL4, we develop a new technology to generate fresh names occurring in Böhm trees. We also simplify Barendregt’s approach, avoiding comparing Böhm trees, and leveraging more modern proofs about η-reduction (due to Takahashi). Along the way, we also present the first mechanised proof that terms having head-normal forms are exactly those that are solvable (due to Wadsworth).
Cite as

Chun Tian and Michael Norrish. Mechanising Böhm Trees and λη-Completeness. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tian_et_al:LIPIcs.ITP.2025.28,
  author =	{Tian, Chun and Norrish, Michael},
  title =	{{Mechanising B\"{o}hm Trees and \lambda\eta-Completeness}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.28},
  URN =		{urn:nbn:de:0030-drops-246269},
  doi =		{10.4230/LIPIcs.ITP.2025.28},
  annote =	{Keywords: untyped \lambda-calculus, B\"{o}hm trees, higher-order logic, theorem proving}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.29
Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs

Authors: Jérémy Thibault, Joseph Lenormand, and Cătălin Hriţcu

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Researchers aim to build secure compilation chains enforcing that if there is no attack a source context can mount against a source program then there is also no attack an adversarial target context can mount against the compiled program. Proving that these compilation chains are secure is, however, challenging, and involves a non-trivial back-translation step: for any attack a target context mounts against the compiled program one has to exhibit a source context mounting the same attack against the source program. We describe a novel back-translation technique, which results in simpler proofs that can be more easily mechanized in a proof assistant. Given a finite set of finite trace prefixes, capturing the interaction recorded during an attack between a target context and the compiled program, we build a call-return tree that we back-translate into a source context producing the same trace prefixes. We use state in the generated source context to record the current location in the call-return tree. The back-translation is done in several small steps, each adding to the tree new information describing how the location should change depending on how the context regains control. To prove this back-translation correct we give semantics to every intermediate call-return tree language, using ghost state to store information and explicitly enforce execution invariants. We prove several small forward simulations, basically seeing the back-translation as a verified nanopass compiler. Thanks to this modular structure, we are able to mechanize this complex back-translation and its correctness proof in the Rocq prover without too much effort.
Cite as

Jérémy Thibault, Joseph Lenormand, and Cătălin Hriţcu. Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{thibault_et_al:LIPIcs.ITP.2025.29,
  author =	{Thibault, J\'{e}r\'{e}my and Lenormand, Joseph and Hri\c{t}cu, C\u{a}t\u{a}lin},
  title =	{{Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.29},
  URN =		{urn:nbn:de:0030-drops-246272},
  doi =		{10.4230/LIPIcs.ITP.2025.29},
  annote =	{Keywords: secure compilation, back-translation, machine-checked proofs, Rocq, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.31
On Verifying Secret Control Flow Elimination

Authors: David Knothe and Oliver Bringmann

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Many countermeasures against timing side-channel attacks have been developed in recent years, including tools to verify that code or a binary is constant-time, compilers or languages that compile into constant-time code, and a formal verification of a compiler that retains the constant-time property. We take a first step toward formally verifying a C compiler that eliminates control-flow-induced timing side channels. Specifically, we extend CompCert with Partial Control-Flow Linearization (PCFL) [Simon Moll and Sebastian Hack, 2018], a global if-conversion algorithm that was repurposed by Soares et al. [Luigi Soares et al., 2023] for removing timing side channels. Our transformation is split into multiple steps, separating linearization from instruction predication. One of the intermediate states contains the current program points before and after linearization simultaneously and we exploit a postdominance relation between those to show semantic preservation. We give a new proof that PCFL leaves uniform program points untouched and use it to show that our transformation correctly eliminates all secret control flow. Although our transformation currently only supports a subset of C, making it unsuitable for use in production, it gives an insight into how a global graph-based linearization technique like PCFL can be verified in CompCert and thereby shows the challenges and obstacles of this undertaking.
Cite as

David Knothe and Oliver Bringmann. On Verifying Secret Control Flow Elimination. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{knothe_et_al:LIPIcs.ITP.2025.31,
  author =	{Knothe, David and Bringmann, Oliver},
  title =	{{On Verifying Secret Control Flow Elimination}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{31:1--31:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.31},
  URN =		{urn:nbn:de:0030-drops-246299},
  doi =		{10.4230/LIPIcs.ITP.2025.31},
  annote =	{Keywords: CompCert, small-step, linearization, side-channels, constant-time, verification, security, taint analysis}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.32
Program Optimisations via Hylomorphisms for Extraction of Executable Code

Authors: David Castro Perez, Marco Paviotti, and Michael Vollmer

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Generic programming with recursion schemes provides a powerful abstraction for structuring recursion and provides a rigorous reasoning principle for program optimisations which have been successfully applied to compilers for functional languages. Formalising recursion schemes in a type theory offers additional termination guarantees, but it often requires compromising on performance, requiring the assumption of additional axioms, and/or introducing unsafe casts into extracted code. This paper presents the first Rocq formalisation of hylomorphisms allowing for the mechanisation of all recognised recursive algorithms. The key contribution of this paper is that this formalisation is fully axiom-free, and it allows the extraction of safe, idiomatic functional code. We exemplify the framework by formalising a series of algorithms based on different recursive paradigms such as divide-and conquer, dynamic programming, and mutual recursion and demonstrate that the extracted functional code for the programs formalised in our framework is efficient, humanly readable, and runnable. Furthermore, we show the use of the machine-checked proofs of the laws of hylomorphisms to do program optimisations.
Cite as

David Castro Perez, Marco Paviotti, and Michael Vollmer. Program Optimisations via Hylomorphisms for Extraction of Executable Code. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{castroperez_et_al:LIPIcs.ITP.2025.32,
  author =	{Castro Perez, David and Paviotti, Marco and Vollmer, Michael},
  title =	{{Program Optimisations via Hylomorphisms for Extraction of Executable Code}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.32},
  URN =		{urn:nbn:de:0030-drops-246302},
  doi =		{10.4230/LIPIcs.ITP.2025.32},
  annote =	{Keywords: hylomorphisms, program calculation, divide and conquer, fusion}
}
  • Refine by Type
  • 65 Document/PDF
  • 38 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 2 2026
  • 53 2025
  • 1 2024
  • 2 2023
  • 2 2022
  • Show More...

  • Refine by Author
  • 12 Forster, Yannick
  • 5 Kirst, Dominik
  • 4 Carneiro, Mario
  • 3 Kunze, Fabian
  • 2 Accattoli, Beniamino
  • Show More...

  • Refine by Series/Journal
  • 63 LIPIcs
  • 1 OASIcs
  • 1 LITES

  • Refine by Classification
  • 24 Theory of computation → Logic and verification
  • 22 Theory of computation → Type theory
  • 10 Theory of computation → Constructive mathematics
  • 7 Theory of computation → Automated reasoning
  • 6 Security and privacy → Logic and verification
  • Show More...

  • Refine by Keyword
  • 13 Coq
  • 9 Isabelle/HOL
  • 6 computability theory
  • 6 type theory
  • 4 Lean
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact