DROPS

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

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

DOI: 10.4230/LIPIcs.ITP.2025.6

A Natural Language Formalization of Perfectoid Rings in ℕaproche

Authors: Peter Koepke

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

Abstract

This paper describes an experiment to formalize sophisticated mathematics in the ℕaproche proof assistant which uses natural language input and a first-order internal logic. We view this as a contribution to the ongoing discussion whether formal systems for research mathematics require complex, computer-orientated type systems or whether approaches closer to traditional mathematical practices are possible. The formalization also explores the limits of the current ℕaproche system and avenues for further development.

Cite as

Peter Koepke. A Natural Language Formalization of Perfectoid Rings in ℕaproche. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{koepke:LIPIcs.ITP.2025.6,
  author =	{Koepke, Peter},
  title =	{{A Natural Language Formalization of Perfectoid Rings in \mathbb{N}aproche}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{6:1--6:15},
  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.6},
  URN =		{urn:nbn:de:0030-drops-246054},
  doi =		{10.4230/LIPIcs.ITP.2025.6},
  annote =	{Keywords: formal mathematics, formalization, perfectoid rings, controlled natural language, Naproche}
}

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}
}

Document

DOI: 10.4230/LIPIcs.ITP.2025.34

Verification of the CVM Algorithm with a Functional Probabilistic Invariant

Authors: Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, and Yong Kiam Tan

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

Abstract

Estimating the number of distinct elements in a data stream is a classic problem with numerous applications in computer science. We formalize a recent, remarkably simple, randomized algorithm for this problem due to Chakraborty, Vinodchandran, and Meel (called the CVM algorithm). Their algorithm deviated considerably from the state of the art, due to its avoidance of intricate derandomization techniques, while still maintaining a close-to-optimal logarithmic space complexity. Central to our formalization is a new proof technique based on functional probabilistic invariants, which allows us to derive concentration bounds using the Cramér-Chernoff method without relying on independence. This simplifies the formal analysis considerably compared to the original proof by Chakraborty et al. Moreover, our technique opens up the possible algorithm design space; we demonstrate this by introducing and verifying a new variant of the CVM algorithm that is both total and unbiased - neither of which is a property of the original algorithm. In this paper, we introduce the proof technique, describe its use in mechanizing both versions of the CVM algorithm in Isabelle/HOL, and present a supporting formalized library on negatively associated random variables used to verify the latter variant.

Cite as

Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, and Yong Kiam Tan. Verification of the CVM Algorithm with a Functional Probabilistic Invariant. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{karayel_et_al:LIPIcs.ITP.2025.34,
  author =	{Karayel, Emin and Watt, Seng Joe and Khu, Derek and Meel, Kuldeep S. and Tan, Yong Kiam},
  title =	{{Verification of the CVM Algorithm with a Functional Probabilistic Invariant}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{34:1--34: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.34},
  URN =		{urn:nbn:de:0030-drops-246327},
  doi =		{10.4230/LIPIcs.ITP.2025.34},
  annote =	{Keywords: Verification, Isabelle/HOL, Randomized Algorithms, Distinct Elements}
}

50 Search Results for "Keller, Chantal"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message