93 Search Results for "Nipkow, Tobias"

Volume

LIPIcs, Volume 382

17th International Conference on Interactive Theorem Proving (ITP 2026)

ITP 2026, Lisbon, Portugal, July 26-29, 2026

Editors: Ekaterina Komendantskaya and Tobias Nipkow

Document
Complete Volume
DOI: 10.4230/LIPIcs.ITP.2026
LIPIcs, Volume 382, ITP 2026, Complete Volume

Authors: Ekaterina Komendantskaya and Tobias Nipkow

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
LIPIcs, Volume 382, ITP 2026, Complete Volume
Cite as

17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 1-652, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Proceedings{komendantskaya_et_al:LIPIcs.ITP.2026,
  title =	{{LIPIcs, Volume 382, ITP 2026, Complete Volume}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{1--652},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026},
  URN =		{urn:nbn:de:0030-drops-273071},
  doi =		{10.4230/LIPIcs.ITP.2026},
  annote =	{Keywords: LIPIcs, Volume 382, ITP 2026, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ITP.2026.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Ekaterina Komendantskaya and Tobias Nipkow

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{komendantskaya_et_al:LIPIcs.ITP.2026.0,
  author =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.0},
  URN =		{urn:nbn:de:0030-drops-273066},
  doi =		{10.4230/LIPIcs.ITP.2026.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2026.1
Nitro Isolation Engine: Formally Verifying a Production Hypervisor (Invited Talk)

Authors: Hanno Becker, Nathan Chong, Robert Dockins, Jim Grundy, Jason Hu, Ike Mulder, Dominic P. Mulligan, Paul Mure, Bryan Parno, Lawrence C. Paulson, and Konrad Slind

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
Cloud computing relies on hypervisors to enforce isolation between co-tenanted virtual machines. Hypervisors are therefore critical security infrastructure, and assurance of their correctness is paramount. Traditional engineering techniques - code review, testing, fuzzing - provide strong assurance but cannot exhaustively verify that isolation holds across all possible execution paths. Formal verification extends and complements these approaches by establishing mathematical guarantees about system behaviour. This talk presents our experience applying interactive theorem proving to verify a production hypervisor component: the Nitro Isolation Engine. This is a trusted, minimalist computing base written in Rust, enforcing isolation between virtual machines on AWS Graviton5 EC2 instances. Designed for verification from inception, we have specified the intended behaviour of this component and verified correctness in the Isabelle/HOL interactive theorem prover, producing approximately 330,000 lines of machine-checked models and proofs, and establishing three key classes of property: 1) Functional correctness: The system behaves as specified for all operations including virtual machine creation, memory mapping, and abort handling. Our total verification approach additionally establishes memory-safety, termination, and absence of runtime errors. 2) Confidentiality: A noninterference-style property demonstrates that guest virtual machine state remains hidden from an expansive definition of observer monitoring system actions, formalised as indistinguishability preservation up to permitted declassification flows. 3) Integrity: Guest virtual machine private state is unaffected by operations on distinct virtual machines. Currently, our proof coverage extends to verification of the core virtual machine-management hypercalls, guest power management, various utility hypercalls, and a subset of data, instruction, and asynchronous abort handling, and will continue to expand to cover more functionality including PCI device management and virtual GIC (Generic Interrupt Controller) handling. The talk will discuss the verification approach, key proof techniques, and challenges in applying formal methods to production systems. Note that this work builds on decades of academic research across interactive theorem proving, formal specification, separation logic and its automation, and programming language semantics.
Cite as

Hanno Becker, Nathan Chong, Robert Dockins, Jim Grundy, Jason Hu, Ike Mulder, Dominic P. Mulligan, Paul Mure, Bryan Parno, Lawrence C. Paulson, and Konrad Slind. Nitro Isolation Engine: Formally Verifying a Production Hypervisor (Invited Talk). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.ITP.2026.1,
  author =	{Becker, Hanno and Chong, Nathan and Dockins, Robert and Grundy, Jim and Hu, Jason and Mulder, Ike and Mulligan, Dominic P. and Mure, Paul and Parno, Bryan and Paulson, Lawrence C. and Slind, Konrad},
  title =	{{Nitro Isolation Engine: Formally Verifying a Production Hypervisor}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.1},
  URN =		{urn:nbn:de:0030-drops-269757},
  doi =		{10.4230/LIPIcs.ITP.2026.1},
  annote =	{Keywords: Isabelle/HOL, Rust, verification, separation logic, hypervisors}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2026.2
Developing a Quantum Crypto Theorem Prover from Scratch (Invited Talk)

Authors: Dominique Unruh

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
We describe our experience developing qrhl-tool, a theorem prover for verifying quantum cryptographic protocols, both in the post-quantum and the full quantum setting. The tool is built around quantum relational Hoare logic (qRHL), a relational program logic for reasoning about pairs of quantum programs in the style of game-based cryptographic proofs. We discuss the design choices underlying the tool: in particular, a hybrid architecture that delegates ambient-logic reasoning to Isabelle/HOL while qrhl-tool itself handles qRHL judgments and the program language; an advanced memoization mechanism (hashed computations) that enables efficient incremental proof checking; and a deliberate path towards a foundational implementation. We walk through a small worked example (the hardness of inverting f∘f given a one-way permutation f) to illustrate how these pieces fit together in practice. Along the way we highlight what we got right, what we got wrong, and which limitations (procedure parameters, local variables, runtime reasoning) we would approach differently if starting over today.
Cite as

Dominique Unruh. Developing a Quantum Crypto Theorem Prover from Scratch (Invited Talk). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{unruh:LIPIcs.ITP.2026.2,
  author =	{Unruh, Dominique},
  title =	{{Developing a Quantum Crypto Theorem Prover from Scratch}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{2:1--2:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.2},
  URN =		{urn:nbn:de:0030-drops-269763},
  doi =		{10.4230/LIPIcs.ITP.2026.2},
  annote =	{Keywords: Formalized mathematics, functional analysis, bounded operators}
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.3
Complex Bounded Operators in Isabelle/HOL

Authors: Dominique Unruh and José Manuel Rodríguez Caballero

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
We present a formalization of bounded operators on complex vector spaces in Isabelle/HOL. Our formalization contains material on complex vector spaces (normed spaces, Banach spaces, Hilbert spaces) that complements and goes beyond the developments of real vectors spaces in the Isabelle/HOL standard library. We define the type of bounded operators between complex vector spaces (cblinfun) and develop the theory of unitaries, projectors, extension of bounded linear functions (BLT theorem), adjoints, Loewner order, closed subspaces and more. For the finite-dimensional case, we provide code generation support by identifying finite-dimensional operators with matrices as formalized in the Jordan_Normal_Form AFP entry.
Cite as

Dominique Unruh and José Manuel Rodríguez Caballero. Complex Bounded Operators in Isabelle/HOL. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{unruh_et_al:LIPIcs.ITP.2026.3,
  author =	{Unruh, Dominique and Caballero, Jos\'{e} Manuel Rodr{\'\i}guez},
  title =	{{Complex Bounded Operators in Isabelle/HOL}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{3:1--3:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.3},
  URN =		{urn:nbn:de:0030-drops-269772},
  doi =		{10.4230/LIPIcs.ITP.2026.3},
  annote =	{Keywords: Formalized mathematics, functional analysis, bounded operators}
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.4
Formally Verified Liveness with Multiparty Session Types in Rocq

Authors: Omer Keskin, Nobuko Yoshida, and Rob van Glabbeek

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
Multiparty session types (MPST) offer a framework for the description of communication-based protocols involving multiple participants. In the top-down approach to MPST, the communication pattern of the session is described using a global type. Then the global type is projected on to a local type for each participant, and the individual processes making up the session are type-checked against these projections. Typed sessions possess certain desirable properties such as safety, deadlock-freedom and liveness. In this work, we present the first mechanised proof of liveness for synchronous multiparty session types in the Rocq Proof Assistant. Building on recent work, we represent global and local types as coinductive trees using the Paco library. We use a coinductively defined subtyping relation on local types together with another coinductively defined plain-merge projection relation relating local and global types. We then associate collections of local types, or local type environments, with global types using these projection and subtyping relations, and prove an operational correspondence between a local type environment and its associated global type. We utilise this association relation to prove the safety and liveness of associated local type environments and, consequently, the multiparty sessions typed by these environments. Besides clarifying the often informal proofs found in the MPST literature, our Rocq mechanisation also enables the certification of liveness properties of communication protocols. Our contribution amounts to around 14K lines of Rocq code, available at https://github.com/omerskeskin/mpstlive.
Cite as

Omer Keskin, Nobuko Yoshida, and Rob van Glabbeek. Formally Verified Liveness with Multiparty Session Types in Rocq. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{keskin_et_al:LIPIcs.ITP.2026.4,
  author =	{Keskin, Omer and Yoshida, Nobuko and van Glabbeek, Rob},
  title =	{{Formally Verified Liveness with Multiparty Session Types in Rocq}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.4},
  URN =		{urn:nbn:de:0030-drops-269787},
  doi =		{10.4230/LIPIcs.ITP.2026.4},
  annote =	{Keywords: Multiparty Session Types, Liveness, Safety, Fairness, Deadlock-Freedom, Endpoint Projection, Subtyping, Rocq, Coinduction, Property Verification}
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.5
Enhancing Interactive Theorem Prover Error Messages with Hints

Authors: Maria Khakimova, Sára Juhošová, Jaro Reinders, and Jesper Cockx

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
Interactive theorem provers (ITPs) are promising tools for ensuring program correctness, but users often complain about their poor usability and steep learning curve. A common complaint, especially among new users, are confusing error messages that expose details of the ITP’s underlying theory or implementation details. In this work, we investigate how adding hints to three types of scope and type checking error messages in the Agda ITP affects the new users' debugging experience. We evaluate the effectiveness and perceived helpfulness of those error messages by conducting a between-subjects user study where we provide a series of Agda code snippets, each containing a single error that the participants have to fix based on the error message. We measure the success rate, time taken to fix the error, and perceived helpfulness for each code snippet with the original as well as the enhanced error message and determine the statistical significance of adding the hint. Our results show that correct hints can improve the success rate and time taken to fix the error, and that error messages with hints are rated significantly more helpful than those without. Additionally, we find that while error messages with incorrect hints are often rated as more misleading, they do not significantly impact the success rate or time taken to fix the error. These results show that adding hints to error messages is a viable step on the path towards making ITPs more widely accessible.
Cite as

Maria Khakimova, Sára Juhošová, Jaro Reinders, and Jesper Cockx. Enhancing Interactive Theorem Prover Error Messages with Hints. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{khakimova_et_al:LIPIcs.ITP.2026.5,
  author =	{Khakimova, Maria and Juho\v{s}ov\'{a}, S\'{a}ra and Reinders, Jaro and Cockx, Jesper},
  title =	{{Enhancing Interactive Theorem Prover Error Messages with Hints}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.5},
  URN =		{urn:nbn:de:0030-drops-269791},
  doi =		{10.4230/LIPIcs.ITP.2026.5},
  annote =	{Keywords: Agda, error messages, hints, new users}
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.6
Lazy Proof Automation for Separation Logic

Authors: Valentin Mikhalchuk, Vladimir Gladshtein, and Ilya Sergey

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
Separation Logic is an established formalism for deductive verification of heap-manipulating programs. Proofs of symbolic heap entailment, an analogue of the ordinary logical implication, are amongst the most common reasoning steps in Separation Logic, and many existing heap verifiers provide automation for discharging valid heap entailments. We observe that existing techniques for automating entailment proofs in foundational Separation Logic verifiers embedded into provers such as Rocq, suffer from three main drawbacks: (a) poor performance due to metaprogramming overhead, (b) limited expressivity, and (c) restricted extensibility. To address these shortcomings, we propose lazy proof automation - an approach to entailment proofs inspired by translation validation. Our key idea is to implement an entailment checker as a combination of (1) an efficient but unverified prover, suitable for fast-paced interactive proofs, and (2) a proof reconstruction procedure that takes the prover’s trace and produces a certificate of entailment validity that can be checked a posteriori. We implemented these ideas in Yolo - a generic and extensible heap entailment prover built in Lean. We instantiate Yolo for two Lean-embedded Separation Logics and show its practical benefits, both in terms of user experience and proof-checking speed, compared with the automation available in state-of-the-art foundational Separation Logics.
Cite as

Valentin Mikhalchuk, Vladimir Gladshtein, and Ilya Sergey. Lazy Proof Automation for Separation Logic. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{mikhalchuk_et_al:LIPIcs.ITP.2026.6,
  author =	{Mikhalchuk, Valentin and Gladshtein, Vladimir and Sergey, Ilya},
  title =	{{Lazy Proof Automation for Separation Logic}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.6},
  URN =		{urn:nbn:de:0030-drops-269801},
  doi =		{10.4230/LIPIcs.ITP.2026.6},
  annote =	{Keywords: Lean, proof engineering, meta-programming}
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.7
Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations

Authors: Ricardo Almeida, Blair Archibald, Basile Pesin, and Michele Sevegnani

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
Commutative regular expressions describe sets of unordered words, and are used, for example, when building type systems for process calculi. In these applications, an important operation is finding the intersection of two expressions, but no algorithm currently exists. We remedy this by proposing an algorithm for computing intersections of commutative regular expressions, which we implement and prove correct in the Rocq prover. The algorithm encodes the intersection of two expressions as systems of linear Diophantine equations, and extracts from their solution an intersection expression. To solve these systems we implement and verify the algorithm proposed by Contejean and Devie. We detail the implementation of the intersection algorithm, highlight essential aspects of the proofs (including the complex proof of termination of the equation system solver), and evaluate the OCaml-extracted solver on random and real-world commutative regular expressions.
Cite as

Ricardo Almeida, Blair Archibald, Basile Pesin, and Michele Sevegnani. Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{almeida_et_al:LIPIcs.ITP.2026.7,
  author =	{Almeida, Ricardo and Archibald, Blair and Pesin, Basile and Sevegnani, Michele},
  title =	{{Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.7},
  URN =		{urn:nbn:de:0030-drops-269813},
  doi =		{10.4230/LIPIcs.ITP.2026.7},
  annote =	{Keywords: commutative regular expressions, linear Diophantine equations, interactive theorem provers, Rocq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.8
Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley’s Entropy Integral

Authors: Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, and Naoto Onda

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
Understanding and certifying the generalization performance of machine learning algorithms - i.e. obtaining theoretical estimates of the test error from the training error - is a central theme of statistical learning theory. Among the many complexity measures used to derive such guarantees, Rademacher complexity yields sharp, data-dependent bounds that apply well beyond classical VC-dimension theory. In this study, we formalize the generalization error bound by Rademacher complexity in Lean 4, building on measure-theoretic probability theory available in the Mathlib library. Our development provides a mechanically-checked pipeline from the definitions of empirical and expected Rademacher complexity, through a formal symmetrization argument and a bounded-differences analysis, to high-probability uniform deviation bounds via a formally proved McDiarmid inequality. A key technical contribution is a reusable mechanism for lifting results from countable hypothesis classes (where measurability of suprema is straightforward in Mathlib) to separable topological index sets via a reduction to a countable dense subset. As worked applications of the abstract theorem, we mechanize standard empirical Rademacher bounds for linear predictors under 𝓁₂ and 𝓁₁ regularizations, and we also formalize a Dudley-type entropy integral bound based on covering numbers and a chaining construction.
Cite as

Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, and Naoto Onda. Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley’s Entropy Integral. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{sonoda_et_al:LIPIcs.ITP.2026.8,
  author =	{Sonoda, Sho and Kasaura, Kazumi and Mizuno, Yuma and Tsukamoto, Kei and Onda, Naoto},
  title =	{{Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley’s Entropy Integral}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.8},
  URN =		{urn:nbn:de:0030-drops-269824},
  doi =		{10.4230/LIPIcs.ITP.2026.8},
  annote =	{Keywords: Lean, generalization error bound, Rademacher complexity, McDiarmid’s inequality, Hoeffding’s lemma, symmetrization arguments, chaining, Dudley’s entropy integral}
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.9
Functional Correctness of an Optimized Modular Inversion Algorithm

Authors: Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, and Tomás Vallejos Parada

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
This article describes the first mechanized proof of functional correctness of an algorithm due to Pornin (2020), for computing modular inverses via an optimized extended binary GCD algorithm. This algorithm is widely used in cryptography applications, due to its speed and constant-timeness. But this speed comes from the use of approximate computations during its loop iterations. In particular, the pen-and-paper proof of the fact that sufficiently many loop iterations were performed is especially intricate (and the originally published version was actually wrong), which negatively impacts the trust in the applications that rely on the algorithm. In this work, we expand the notes provided in the original description by Pornin into a complete formal proof. We discuss the challenges raised by its mechanization, which eventually relies on the collaboration of deductive program verification and interactive theorem proving through the use of the tools Rocq and Why3.
Cite as

Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, and Tomás Vallejos Parada. Functional Correctness of an Optimized Modular Inversion Algorithm. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{mahboubi_et_al:LIPIcs.ITP.2026.9,
  author =	{Mahboubi, Assia and Melquiond, Guillaume and Strub, Pierre-Yves and Vallejos Parada, Tom\'{a}s},
  title =	{{Functional Correctness of an Optimized Modular Inversion Algorithm}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.9},
  URN =		{urn:nbn:de:0030-drops-269839},
  doi =		{10.4230/LIPIcs.ITP.2026.9},
  annote =	{Keywords: deductive program verification, modular inversion algorithm, formal verification, Rocq, Why3}
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.10
Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL

Authors: Fang Yan, Benoît Ballenghien, Simon Foster, Ana Cavalcanti, James Baxter, and Burkhart Wolff

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
We present a theorem-proving-based technique for verifying deadlock freedom of CSP-style concurrent models in Isabelle/HOL. The approach addresses challenges that are difficult to handle using model checking alone, including infinite state spaces, compositional reasoning in the presence of shared variables, and the need for mechanised proofs. Our main contribution is a coinductive characterisation of deadlock freedom that is equivalent to the standard CSP refinement-based definition, but is more amenable to automated reasoning in an interactive theorem prover. To support reasoning about shared variables, we introduce an assume–guarantee strategy that enforces invariants within transition semantics. The technique is generally applicable to CSP specifications that model shared variables using standard CSP constructs. In particular, we consider the semantics of RoboChart, a domain-specific modelling language for robotic control software, which we mechanise in Isabelle via a shallow embedding in HOL-CSP, and implement automated proof methods. The approach is evaluated on three case studies, including two RoboChart models of industrial robotic systems.
Cite as

Fang Yan, Benoît Ballenghien, Simon Foster, Ana Cavalcanti, James Baxter, and Burkhart Wolff. Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{yan_et_al:LIPIcs.ITP.2026.10,
  author =	{Yan, Fang and Ballenghien, Beno\^{i}t and Foster, Simon and Cavalcanti, Ana and Baxter, James and Wolff, Burkhart},
  title =	{{Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{10:1--10:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.10},
  URN =		{urn:nbn:de:0030-drops-269849},
  doi =		{10.4230/LIPIcs.ITP.2026.10},
  annote =	{Keywords: process algebra, Isabelle/HOL, automated proof methods, deadlock freedom}
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.11
Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language

Authors: Vladimir Gladshtein and K. Rustan M. Leino

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
Intermediate Verification Languages (IVLs) play the same role in verification as Intermediate Representations in compilation, a layer that separates a verifier’s language-specific front-end from its logic automation back-end. Successful IVL tools such as Boogie, Why3, and Viper generate Verification Conditions (VCs) that are sent to an SMT solver. The verifier output can be trusted only if these VCs are sound with respect to the formal semantics of the IVL. Formalizing the semantics of IVLs and verifying the soundness of corresponding VC Generators with respect to this semantics is challenging if one wants to model realistic features of IVLs such as mutually recursive definitions, lexical variable and control-flow labeled scopes, interpreted and uninterpreted functions, and unbounded loops. B3 is a new IVL. This paper presents a formalization of B3’s semantics, a VC Generator for the language, and a soundness proof that these two correspond. A key practical contribution of this work is that all three components are authored in the Dafny programming language and verifier. This makes it easy for a tool maintainer to maneuver between the semantic definitions, the proofs, and the VCG’s executable code. The key theoretical contribution of the work is a methodology to split the IVL’s semantic encodings into two layers of abstraction to cover realistic aspects of the semantics, while keeping the proofs amenable to automation. Optimized for Dafny-style automation, the first layer is used to verify the correctness of the VC Generator procedure. Optimized for expressiveness, the second layer is used to capture the semantics in a natural way.
Cite as

Vladimir Gladshtein and K. Rustan M. Leino. Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{gladshtein_et_al:LIPIcs.ITP.2026.11,
  author =	{Gladshtein, Vladimir and Leino, K. Rustan M.},
  title =	{{Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.11},
  URN =		{urn:nbn:de:0030-drops-269855},
  doi =		{10.4230/LIPIcs.ITP.2026.11},
  annote =	{Keywords: Intermediate verification language, Soundness, Verification, B3, Dafny, SMT solvers}
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.12
TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq

Authors: Johann Rosain and Julie Cailler

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
The free-variable tableau method has been widely used in order to automate proofs in multiple kinds of logics. Many automated theorem provers rely on this approach, either because it is the only available method - e.g. in certain modal logics - or because it facilitates the generation of proof certificates. However, as far as the authors know, its results have never been formalized in a proof assistant. In this paper, we present TableauxRocq, a deep embedding of free-variable first-order tableaux in the Rocq prover. The formalized calculus is proved sound and provides a modular Skolemization system that enables the use of Skolemization-based optimizations. Moreover, we show how TableauxRocq can be used as a certifier for automated theorem provers by adapting the Goeland prover - that can already output Rocq terms - to output proofs in the TableauxRocq format. By using the power of reflection, thereby providing a fully certified proof checker for free, we show that Goeland’s exported Rocq terms and TableauxRocq’s proof certificates can be checked in a similar time frame without proof optimizations, and that the latter has strictly better performances in presence of Skolemization-related optimizations.
Cite as

Johann Rosain and Julie Cailler. TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{rosain_et_al:LIPIcs.ITP.2026.12,
  author =	{Rosain, Johann and Cailler, Julie},
  title =	{{TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{12:1--12:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.12},
  URN =		{urn:nbn:de:0030-drops-269869},
  doi =		{10.4230/LIPIcs.ITP.2026.12},
  annote =	{Keywords: The Rocq Prover, First-Order Tableaux, Automated Reasoning, Interoperability, Proof Translation}
}
  • Refine by Type
  • 92 Document/PDF
  • 35 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 41 2026
  • 33 2025
  • 2 2024
  • 3 2023
  • 1 2022
  • Show More...

  • Refine by Author
  • 14 Nipkow, Tobias
  • 5 Giesl, Jürgen
  • 4 Hähnle, Reiner
  • 3 Abdulaziz, Mohammad
  • 3 Avigad, Jeremy
  • Show More...

  • Refine by Series/Journal
  • 81 LIPIcs
  • 4 OASIcs
  • 1 DagRep
  • 6 DagSemProc

  • Refine by Classification
  • 32 Theory of computation → Logic and verification
  • 15 Software and its engineering → Formal software verification
  • 11 Theory of computation → Type theory
  • 10 Theory of computation → Automated reasoning
  • 7 Theory of computation → Equational logic and rewriting
  • Show More...

  • Refine by Keyword
  • 16 Isabelle/HOL
  • 7 Isabelle
  • 7 Lean
  • 6 Rocq
  • 6 Verification
  • 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