6 Search Results for "Ebner, Gabriel"

Document
DOI: 10.4230/LIPIcs.ITP.2025.16
Finiteness of Symbolic Derivatives in Lean

Authors: Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, and Gabriel Ebner

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

Abstract
Brzozowski proved that the set of derivatives of any regular expression is finite modulo associativity, idempotence and, notably, commutativity of the union operator. We extend this result to the case of symbolic location based derivatives, for which we prove finiteness of the state space by quotienting only by associativity, deduplication and idempotence (ADI); the fact that we don't use commutativity allows for this result to carry over to the derivative based backtracking (PCRE) match semantics, where the union operator is noncommutative. Furthermore, we consider regular expressions extended with lookarounds, intersection, and negation. We also show that our method for proving finiteness allows us to include certain simplification rules in the derivative operation while preserving finiteness. The finiteness proof is constructive: given an expression R, we construct a finite set that is an overapproximation (modulo ADI) of the set of derivatives of R. We reuse some of the infrastructure provided in previous formalization efforts for regular expressions in Lean 4, showing the flexibility and reusability of the framework.
Cite as

Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, and Gabriel Ebner. Finiteness of Symbolic Derivatives in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zhuchko_et_al:LIPIcs.ITP.2025.16,
  author =	{Zhuchko, Ekaterina and Maarand, Hendrik and Veanes, Margus and Ebner, Gabriel},
  title =	{{Finiteness of Symbolic Derivatives in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{16:1--16: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.16},
  URN =		{urn:nbn:de:0030-drops-246144},
  doi =		{10.4230/LIPIcs.ITP.2025.16},
  annote =	{Keywords: Lean, regular languages, lookarounds, derivatives, finiteness}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.22
Formalizing Splitting in Isabelle/HOL

Authors: Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret

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

Abstract
We describe the formalization in Isabelle/HOL of a framework for splitting, a theorem proving technique that extends saturation-based calculi with branching abilities. The framework preserves the completeness of the original calculus. We focus here on the simplest splitting model and provide an extension of the ordered resolution calculus with a variant of splitting called Lightweight AVATAR.
Cite as

Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret. Formalizing Splitting in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bergeron_et_al:LIPIcs.ITP.2025.22,
  author =	{Bergeron, Ghilain and Krasnopol, Florent and Tourret, Sophie},
  title =	{{Formalizing Splitting in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{22:1--22: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.22},
  URN =		{urn:nbn:de:0030-drops-246208},
  doi =		{10.4230/LIPIcs.ITP.2025.22},
  annote =	{Keywords: Isabelle/HOL, saturation-based calculi, splitting}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.10
Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory

Authors: Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We present Duper, a proof-producing theorem prover for Lean based on the superposition calculus. Duper can be called directly as a terminal tactic in interactive Lean proofs, but is also designed with proof reconstruction for a future Lean hammer in mind. In this paper, we describe Duper’s underlying approach to proof search and proof reconstruction with a particular emphasis on the challenges of working in a dependent type theory. We also compare Duper’s performance to Metis' on pre-existing benchmarks to give evidence that Duper is performant enough to be useful for proof reconstruction in a hammer.
Cite as

Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{clune_et_al:LIPIcs.ITP.2024.10,
  author =	{Clune, Joshua and Qian, Yicheng and Bentkamp, Alexander and Avigad, Jeremy},
  title =	{{Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{10:1--10:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.10},
  URN =		{urn:nbn:de:0030-drops-207381},
  doi =		{10.4230/LIPIcs.ITP.2024.10},
  annote =	{Keywords: proof search, automatic theorem proving, interactive theorem proving, Lean, dependent type theory}
}
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.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
DOI: 10.4230/LIPIcs.ITP.2021.4
A Graphical User Interface Framework for Formal Verification

Authors: Edward W. Ayers, Mateja Jamnik, and W. T. Gowers

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
We present the "ProofWidgets" framework for implementing general user interfaces (UIs) within an interactive theorem prover. The framework uses web technology and functional reactive programming, as well as metaprogramming features of advanced interactive theorem proving (ITP) systems to allow users to create arbitrary interactive UIs for representing the goal state. Users of the framework can create GUIs declaratively within the ITP’s metaprogramming language, without having to develop in multiple languages and without coordinated changes across multiple projects, which improves development time for new designs of UI. The ProofWidgets framework also allows UIs to make use of the full context of the theorem prover and the specialised libraries that ITPs offer, such as methods for dealing with expressions and tactics. The framework includes an extensible structured pretty-printing engine that enables advanced interaction with expressions such as interactive term rewriting. We exemplify the framework with an implementation for the https://leanprover-community.github.io. The framework is already in use by hundreds of contributors to the Lean mathematical library.
Cite as

Edward W. Ayers, Mateja Jamnik, and W. T. Gowers. A Graphical User Interface Framework for Formal Verification. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ayers_et_al:LIPIcs.ITP.2021.4,
  author =	{Ayers, Edward W. and Jamnik, Mateja and Gowers, W. T.},
  title =	{{A Graphical User Interface Framework for Formal Verification}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{4:1--4:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.4},
  URN =		{urn:nbn:de:0030-drops-138996},
  doi =		{10.4230/LIPIcs.ITP.2021.4},
  annote =	{Keywords: User Interfaces, ITP}
}
  • Refine by Type
  • 6 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 2 2024
  • 1 2023
  • 1 2021

  • Refine by Author
  • 2 Ayers, Edward W.
  • 2 Ebner, Gabriel
  • 1 Avigad, Jeremy
  • 1 Bentkamp, Alexander
  • 1 Bergeron, Ghilain
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs

  • Refine by Classification
  • 2 Software and its engineering → Functional languages
  • 1 Computing methodologies → Theorem proving algorithms
  • 1 Human-centered computing → Visualization systems and tools
  • 1 Security and privacy → Logic and verification
  • 1 Software and its engineering → Software usability
  • Show More...

  • Refine by Keyword
  • 4 Lean
  • 2 interactive theorem proving
  • 1 ITP
  • 1 Isabelle/HOL
  • 1 User Interfaces
  • 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