42 Search Results for "de Moura, Leonardo"

Volume

LIPIcs, Volume 237

13th International Conference on Interactive Theorem Proving (ITP 2022)

ITP 2022, August 7-10, 2022, Haifa, Israel

Editors: June Andronick and Leonardo de Moura

Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2024.3
Lean: Past, Present, and Future (Invited Talk)

Authors: Sebastian Ullrich

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
The Lean programming language and theorem prover project is celebrating its tenth birthday this year, having been started by Leonardo de Moura at Microsoft Research and first release as Lean 0.1 in 2014. In this invited talk, I will review Lean’s history and unique features and discuss our roadmap for its bright future. Corresponding to its major versions ranging from Lean 0.1 to the current version of Lean 4, the focus of the Lean project has evolved over the years. Initially intended as a platform for developing white-box automation, in contrast to the usual black-box approach of stand-alone SMT solvers [de Moura and Passmore, 2013], the system gathered more conventional features of dependently-typed interactive theorem provers as well as an initial crowd of interested mathematicians and computer scientists with its first official release as Lean 2 in 2015 [Leonardo de Moura et al., 2015]. Lean 3 in 2017 introduced user-extensible automation by extending Lean from a specification language to an accessible metaprogramming language [Gabriel Ebner et al., 2017], further accelerating growth of its mathematical library that was spun out into the separate Mathlib project [{The mathlib Community}, 2020]. Spurred by the success but also limitations of this extensibility, we started work on the next version Lean 4 in 2018 [Leonardo de Moura and Sebastian Ullrich, 2021] with the goal of turning Lean into a general-purpose programming language that would allow us to reimplement Lean in Lean itself and thereby make many more aspects of the system user-extensible, in a more efficient manner [Sebastian Ullrich, 2023]. This to date largest rework of Lean’s implementation was completed in 2023 with the official release of Lean 4.0.0, further supporting Mathlib’s growth to more than 1.5 million lines of code at the time of writing as well as improving support for many other applications such as software verification. In 2023, Lean also saw its largest organizational change when Leo and I created the Lean Focused Research Organization (FRO) to bundle and support development of Lean in a dedicated organization for the first time. Thanks to gracious support from philanthropic sponsors, an unprecedented number of currently twelve people now work on the evolution of Lean at the Lean FRO. And there is much left to do: with our new team size, we can now support development on much more than only core features, such as documentation, a robust standard library, and user interfaces and experience as well as a return to the original topic of advanced proof automation. The Lean FRO is committed to ensuring and extending Lean’s applicability in education, research, and industry and to leading it into the next decade of Lean development and beyond.
Cite as

Sebastian Ullrich. Lean: Past, Present, and Future (Invited Talk). In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ullrich:LIPIcs.FSCD.2024.3,
  author =	{Ullrich, Sebastian},
  title =	{{Lean: Past, Present, and Future}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{3:1--3:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.3},
  URN =		{urn:nbn:de:0030-drops-203328},
  doi =		{10.4230/LIPIcs.FSCD.2024.3},
  annote =	{Keywords: Lean, interactive theorem proving, focused research organization, history}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.5
The Flower Calculus

Authors: Pablo Donato

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
We introduce the flower calculus, a deep inference proof system for intuitionistic first-order logic inspired by Peirce’s existential graphs. It works as a rewriting system over inductive objects called "flowers", that enjoy both a graphical interpretation as topological diagrams, and a textual presentation as nested sequents akin to coherent formulas. Importantly, the calculus dispenses completely with the traditional notion of symbolic connective, operating solely on nested flowers containing atomic predicates. We prove both the soundness of the full calculus and the completeness of an analytic fragment with respect to Kripke semantics. This provides to our knowledge the first analyticity result for a proof system based on existential graphs, adapting semantic cut-elimination techniques to a deep inference setting. Furthermore, the kernel of rules targetted by completeness is fully invertible, a desirable property for both automated and interactive proof search.
Cite as

Pablo Donato. The Flower Calculus. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 5:1-5:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{donato:LIPIcs.FSCD.2024.5,
  author =	{Donato, Pablo},
  title =	{{The Flower Calculus}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{5:1--5:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.5},
  URN =		{urn:nbn:de:0030-drops-203343},
  doi =		{10.4230/LIPIcs.FSCD.2024.5},
  annote =	{Keywords: deep inference, graphical calculi, existential graphs, intuitionistic logic, Kripke semantics, cut-elimination}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.11
Optimizing a Non-Deterministic Abstract Machine with Environments

Authors: Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Non-deterministic abstract machine (NDAM) is a recent implementation model for programming languages where one must choose among several redexes at each reduction step, like process calculi. These machines can be derived from a zipper semantics, a mix between structural operational semantics and context-based reduction semantics. Such a machine has been generated also for the λ-calculus without a fixed reduction strategy, i.e., with the full non-deterministic β-reduction. In that machine, substitution is an external operation that replaces all the occurrences of a variable at once. Implementing substitution with environments is more low-level and more efficient as variables are replaced only when needed. In this paper, we define a NDAM with environments for the λ-calculus without a fixed reduction strategy. We also introduce other optimizations, including a form of refocusing, and we show that we can restrict our optimized NDAM to recover some of the usual λ-calculus machines, e.g., the Krivine Abstract Machine. Most of the improvements we propose in this work could be applied to other NDAMs as well.
Cite as

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Optimizing a Non-Deterministic Abstract Machine with Environments. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{biernacka_et_al:LIPIcs.FSCD.2024.11,
  author =	{Biernacka, Ma{\l}gorzata and Biernacki, Dariusz and Lenglet, Sergue\"{i} and Schmitt, Alan},
  title =	{{Optimizing a Non-Deterministic Abstract Machine with Environments}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{11:1--11:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.11},
  URN =		{urn:nbn:de:0030-drops-203409},
  doi =		{10.4230/LIPIcs.FSCD.2024.11},
  annote =	{Keywords: Abstract machine, Explicit substitutions, Refocusing}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.21
Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti

Authors: Thiago Felicissimo and Théo Winterhalter

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Proof assistants such as Coq implement a type theory featuring three important features: impredicativity, cumulativity and product covariance. This combination has proven difficult to be expressed in the logical framework Dedukti, and previous attempts have failed in providing an encoding that is proven confluent, sound and conservative. In this work we solve this longstanding open problem by providing an encoding of these three features that we prove to be confluent, sound and to satisfy a restricted (but, we argue, strong enough) form of conservativity. Our proof of confluence is a contribution by itself, and combines various criteria and proof techniques from rewriting theory. Our proof of soundness also contributes a new strategy in which the result is shown in terms of an inverse translation function, fixing a common flaw made in some previous encoding attempts.
Cite as

Thiago Felicissimo and Théo Winterhalter. Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{felicissimo_et_al:LIPIcs.FSCD.2024.21,
  author =	{Felicissimo, Thiago and Winterhalter, Th\'{e}o},
  title =	{{Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{21:1--21:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.21},
  URN =		{urn:nbn:de:0030-drops-203503},
  doi =		{10.4230/LIPIcs.FSCD.2024.21},
  annote =	{Keywords: Dedukti, Rewriting, Confluence, Dependent types, Cumulativity, Universes}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.24
An Extensible User Interface for Lean 4

Authors: Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Contemporary proof assistants rely on complex automation and process libraries with millions of lines of code. At these scales, understanding the emergent interactions between components can be a serious challenge. One way of managing complexity, long established in informal practice, is through varying external representations. For instance, algebraic notation facilitates term-based reasoning whereas geometric diagrams invoke spatial intuition. Objects viewed one way become much simpler than when viewed differently. In contrast, modern general-purpose ITP systems usually only support limited, textual representations. Treating this as a problem of human-computer interaction, we aim to demonstrate that presentations - UI elements that store references to the objects they are displaying - are a fruitful way of thinking about ITP interface design. They allow us to make headway on two fronts - introspection of prover internals and support for diagrammatic reasoning. To this end we have built an extensible user interface for the Lean 4 prover with an associated ProofWidgets 4 library of presentation-based UI components. We demonstrate the system with several examples including type information popups, structured traces, contextual suggestions, a display for algebraic reasoning, and visualizations of red-black trees. Our interface is already part of the core Lean distribution.
Cite as

Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An Extensible User Interface for Lean 4. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{nawrocki_et_al:LIPIcs.ITP.2023.24,
  author =	{Nawrocki, Wojciech and Ayers, Edward W. and Ebner, Gabriel},
  title =	{{An Extensible User Interface for Lean 4}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{24:1--24:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.24},
  URN =		{urn:nbn:de:0030-drops-183991},
  doi =		{10.4230/LIPIcs.ITP.2023.24},
  annote =	{Keywords: user interfaces, human-computer interaction, Lean}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.ITP.2022
LIPIcs, Volume 237, ITP 2022, Complete Volume

Authors: June Andronick and Leonardo de Moura

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
LIPIcs, Volume 237, ITP 2022, Complete Volume
Cite as

13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 1-602, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Proceedings{andronick_et_al:LIPIcs.ITP.2022,
  title =	{{LIPIcs, Volume 237, ITP 2022, Complete Volume}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{1--602},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022},
  URN =		{urn:nbn:de:0030-drops-167080},
  doi =		{10.4230/LIPIcs.ITP.2022},
  annote =	{Keywords: LIPIcs, Volume 237, ITP 2022, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ITP.2022.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: June Andronick and Leonardo de Moura

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

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

13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{andronick_et_al:LIPIcs.ITP.2022.0,
  author =	{Andronick, June and de Moura, Leonardo},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.0},
  URN =		{urn:nbn:de:0030-drops-167097},
  doi =		{10.4230/LIPIcs.ITP.2022.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2022.1
Modelling and Verifying Properties of Biological Neural Networks (Invited Talk)

Authors: Amy Felty

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
In this talk, I present a formal model of biological neural networks and discuss the use of model checking and interactive theorem proving to verify some of their properties. Having a formal model can increase our understanding of the behavior and properties of such networks, as well as provide insight into their response to external factors such as disease, medicine, and environmental changes. We focus on neuronal micro-networks, considering properties of single neurons as well as properties of slightly larger ones called archetypes, which represent specific computational functions. Archetypes, in turn, represent the building blocks of larger more complicated neuronal circuits. I first present work by colleagues on a model checking approach, and then present our joint work on a newer theorem proving approach. Using interactive theorem proving allows us to generalize the kinds of properties that we can prove. This work is joint with Abdorrahim Bahrami and Elisabetta De Maria.
Cite as

Amy Felty. Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{felty:LIPIcs.ITP.2022.1,
  author =	{Felty, Amy},
  title =	{{Modelling and Verifying Properties of Biological Neural Networks}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.1},
  URN =		{urn:nbn:de:0030-drops-167100},
  doi =		{10.4230/LIPIcs.ITP.2022.1},
  annote =	{Keywords: Neuronal networks, Model checking, Theorem proving, Coq}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2022.2
User Interface Design in the HolPy Theorem Prover (Invited Talk)

Authors: Bohua Zhan

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
HolPy is a new interactive theorem prover implemented in Python. It is designed to achieve a small trusted-code-base with externally checkable proofs, writing proof automation using a Python API, and permit a wide variety of user interfaces for different application scenarios. In this talk, I will focus on the design of user interfaces in HolPy. While most interactive theorem provers today use text-based user interfaces, there have been several existing work aiming to build point-and-click interfaces where the user perform actions by clicking on part of the goal or choosing from a menu. In our work, we incorporate into the design extensive proof automation and heuristic suggestion mechanisms, allowing construction of proofs on a large scale using this method. We demonstrate the approach in two common scenarios: general-purpose theorem proving and symbolic computation in mathematics.
Cite as

Bohua Zhan. User Interface Design in the HolPy Theorem Prover (Invited Talk). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{zhan:LIPIcs.ITP.2022.2,
  author =	{Zhan, Bohua},
  title =	{{User Interface Design in the HolPy Theorem Prover}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.2},
  URN =		{urn:nbn:de:0030-drops-167117},
  doi =		{10.4230/LIPIcs.ITP.2022.2},
  annote =	{Keywords: Proof assistants, User interface, Proof automation}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.3
Candle: A Verified Implementation of HOL Light

Authors: Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
This paper presents a fully verified interactive theorem prover for higher-order logic, more specifically: a fully verified clone of HOL Light. Our verification proof of this new system results in an end-to-end correctness theorem that guarantees the soundness of the entire system down to the machine code that executes at runtime. Our theorem states that every exported fact produced by this machine-code program is valid in higher-order logic. Our implementation consists of a read-eval-print loop (REPL) that executes the CakeML compiler internally. Throughout this work, we have strived to make the REPL of the new system provide a user experience as close to HOL Light’s as possible. To this end, we have, e.g., made the new system parse the same variant of OCaml syntax as HOL Light. All of the work described in this paper has been carried out in the HOL4 theorem prover.
Cite as

Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell. Candle: A Verified Implementation of HOL Light. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{abrahamsson_et_al:LIPIcs.ITP.2022.3,
  author =	{Abrahamsson, Oskar and Myreen, Magnus O. and Kumar, Ramana and Sewell, Thomas},
  title =	{{Candle: A Verified Implementation of HOL Light}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{3:1--3:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.3},
  URN =		{urn:nbn:de:0030-drops-167126},
  doi =		{10.4230/LIPIcs.ITP.2022.3},
  annote =	{Keywords: Prover soundness, Higher-order logic, Interactive theorem proving}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.4
Use and Abuse of Instance Parameters in the Lean Mathematical Library

Authors: Anne Baanen

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean’s mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them.
Cite as

Anne Baanen. Use and Abuse of Instance Parameters in the Lean Mathematical Library. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{baanen:LIPIcs.ITP.2022.4,
  author =	{Baanen, Anne},
  title =	{{Use and Abuse of Instance Parameters in the Lean Mathematical Library}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{4:1--4:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.4},
  URN =		{urn:nbn:de:0030-drops-167131},
  doi =		{10.4230/LIPIcs.ITP.2022.4},
  annote =	{Keywords: formalization of mathematics, dependent type theory, typeclasses, algebraic hierarchy, Lean prover}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.5
A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)

Authors: Jagadish Bapanapally and Ruben Gamboa

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
This paper presents a formal proof of the Banach-Tarski theorem in ACL2(r). The Banach-Tarski theorem states that a unit ball can be partitioned into a finite number of pieces that can be rotated to form two identical copies of the ball. We have formalized 3D rotations and generated a free group of 3D rotations of rank 2. In prior work, the non-denumerability of the reals was proved in ACL2 (r), and a version of the Axiom of Choice that can consistently select a representative element from an equivalence class was introduced in ACL2 version 3.1. Using the free group of rotations, and this prior work, we show that the unit sphere can be decomposed into two sets, each equivalent to the original sphere. Then we show that the unit ball except for the origin can be decomposed into two sets each equivalent to the original ball by mapping the points of the unit ball to the points on the sphere. Finally, we handle the origin by rotating the unit ball around an axis such that the origin falls inside the sphere. Seemingly paradoxically, the construction results in two copies of the unit ball.
Cite as

Jagadish Bapanapally and Ruben Gamboa. A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bapanapally_et_al:LIPIcs.ITP.2022.5,
  author =	{Bapanapally, Jagadish and Gamboa, Ruben},
  title =	{{A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{5:1--5:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.5},
  URN =		{urn:nbn:de:0030-drops-167142},
  doi =		{10.4230/LIPIcs.ITP.2022.5},
  annote =	{Keywords: ACL2(r), Banach-Tarski, Rotations}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.6
Dandelion: Certified Approximations of Elementary Functions

Authors: Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
Elementary function operations such as sin and exp cannot in general be computed exactly on today’s digital computers, and thus have to be approximated. The standard approximations in library functions typically provide only a limited set of precisions, and are too inefficient for many applications. Polynomial approximations that are customized to a limited input domain and output accuracy can provide superior performance. In fact, the Remez algorithm computes the best possible approximation for a given polynomial degree, but has so far not been formally verified. This paper presents Dandelion, an automated certificate checker for polynomial approximations of elementary functions computed with Remez-like algorithms that is fully verified in the HOL4 theorem prover. Dandelion checks whether the difference between a polynomial approximation and its target reference elementary function remains below a given error bound for all inputs in a given constraint. By extracting a verified binary with the CakeML compiler, Dandelion can validate certificates within a reasonable time, fully automating previous manually verified approximations.
Cite as

Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin. Dandelion: Certified Approximations of Elementary Functions. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.ITP.2022.6,
  author =	{Becker, Heiko and Tekriwal, Mohit and Darulova, Eva and Volkova, Anastasia and Jeannin, Jean-Baptiste},
  title =	{{Dandelion: Certified Approximations of Elementary Functions}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.6},
  URN =		{urn:nbn:de:0030-drops-167155},
  doi =		{10.4230/LIPIcs.ITP.2022.6},
  annote =	{Keywords: elementary functions, approximation, certificate checking}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.7
The Zoo of Lambda-Calculus Reduction Strategies, And Coq

Authors: Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
We present a generic framework for the specification and reasoning about reduction strategies in the lambda calculus, representable as sets of term decompositions. It is provided as a Coq formalization that features a novel format of phased strategies. It facilitates concise description and algebraic reasoning about properties of reduction strategies. The formalization accommodates many well-known strategies, both weak and strong, such as call by name, call by value, head reduction, normal order, full β-reduction, etc. We illustrate the use of the framework as a tool to inspect and categorize the "zoo" of existing strategies, as well as to discover and study new ones with particular properties.
Cite as

Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab. The Zoo of Lambda-Calculus Reduction Strategies, And Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{biernacka_et_al:LIPIcs.ITP.2022.7,
  author =	{Biernacka, Ma{\l}gorzata and Charatonik, Witold and Drab, Tomasz},
  title =	{{The Zoo of Lambda-Calculus Reduction Strategies, And Coq}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.7},
  URN =		{urn:nbn:de:0030-drops-167165},
  doi =		{10.4230/LIPIcs.ITP.2022.7},
  annote =	{Keywords: Lambda calculus, Reduction strategies, Coq}
}
  • Refine by Author
  • 3 de Moura, Leonardo
  • 2 Andronick, June
  • 2 Biernacka, Małgorzata
  • 2 Chlipala, Adam
  • 2 Gross, Jason
  • Show More...

  • Refine by Classification
  • 12 Theory of computation → Logic and verification
  • 7 Theory of computation → Type theory
  • 6 Theory of computation → Automated reasoning
  • 5 Theory of computation → Higher order logic
  • 5 Theory of computation → Interactive proof systems
  • Show More...

  • Refine by Keyword
  • 8 Coq
  • 5 Lean
  • 4 Isabelle/HOL
  • 3 interactive theorem proving
  • 2 Formal Verification
  • Show More...

  • Refine by Type
  • 41 document
  • 1 volume

  • Refine by Publication Year
  • 36 2022
  • 4 2024
  • 1 2010
  • 1 2023

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact