4 Search Results for "Lorenzen, Anton"

Document
DOI: 10.4230/LIPIcs.ITP.2025.6
A Natural Language Formalization of Perfectoid Rings in ℕaproche

Authors: Peter Koepke

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

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

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

Copy BibTex To Clipboard

@InProceedings{koepke:LIPIcs.ITP.2025.6,
  author =	{Koepke, Peter},
  title =	{{A Natural Language Formalization of Perfectoid Rings in \mathbb{N}aproche}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{6:1--6:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.6},
  URN =		{urn:nbn:de:0030-drops-246054},
  doi =		{10.4230/LIPIcs.ITP.2025.6},
  annote =	{Keywords: formal mathematics, formalization, perfectoid rings, controlled natural language, Naproche}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.4
Substructural Parametricity

Authors: C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.
Cite as

C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning. Substructural Parametricity. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aberle_et_al:LIPIcs.FSCD.2025.4,
  author =	{Aberl\'{e}, C. B. and Crary, Karl and Martens, Chris and Pfenning, Frank},
  title =	{{Substructural Parametricity}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.4},
  URN =		{urn:nbn:de:0030-drops-236193},
  doi =		{10.4230/LIPIcs.FSCD.2025.4},
  annote =	{Keywords: Substructural type systems, logical relations, ordered logic}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.9
Verifying Peephole Rewriting in SSA Compiler IRs

Authors: Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, and Tobias Grosser

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

Abstract
There is an increasing need for domain-specific reasoning in modern compilers. This has fueled the use of tailored intermediate representations (IRs) based on static single assignment (SSA), like in the MLIR compiler framework. Interactive theorem provers (ITPs) provide strong guarantees for the end-to-end verification of compilers (e.g., CompCert). However, modern compilers and their IRs evolve at a rate that makes proof engineering alongside them prohibitively expensive. Nevertheless, well-scoped push-button automated verification tools such as the Alive peephole verifier for LLVM-IR gained recognition in domains where SMT solvers offer efficient (semi) decision procedures. In this paper, we aim to combine the convenience of automation with the versatility of ITPs for verifying peephole rewrites across domain-specific IRs. We formalize a core calculus for SSA-based IRs that is generic over the IR and covers so-called regions (nested scoping used by many domain-specific IRs in the MLIR ecosystem). Our mechanization in the Lean proof assistant provides a user-friendly frontend for translating MLIR syntax into our calculus. We provide scaffolding for defining and verifying peephole rewrites, offering tactics to eliminate the abstraction overhead of our SSA calculus. We prove correctness theorems about peephole rewriting, as well as two classical program transformations. To evaluate our framework, we consider three use cases from the MLIR ecosystem that cover different levels of abstractions: (1) bitvector rewrites from LLVM, (2) structured control flow, and (3) fully homomorphic encryption. We envision that our mechanization provides a foundation for formally verified rewrites on new domain-specific IRs.
Cite as

Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, and Tobias Grosser. Verifying Peephole Rewriting in SSA Compiler IRs. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bhat_et_al:LIPIcs.ITP.2024.9,
  author =	{Bhat, Siddharth and Keizer, Alex and Hughes, Chris and Goens, Andr\'{e}s and Grosser, Tobias},
  title =	{{Verifying Peephole Rewriting in SSA Compiler IRs}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{9:1--9: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.9},
  URN =		{urn:nbn:de:0030-drops-207372},
  doi =		{10.4230/LIPIcs.ITP.2024.9},
  annote =	{Keywords: compilers, semantics, mechanization, MLIR, SSA, regions, peephole rewrites}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.16
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche

Authors: Adrian De Lon, Peter Koepke, and Anton Lorenzen

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

Abstract
Naproche is an emerging natural proof assistant that accepts input in a controlled natural language for mathematics, which we have integrated with LaTeX for ease of learning and to quickly produce high-quality typeset documents. We present a self-contained formalization of the Mutilated Checkerboard Problem in Naproche, following a proof sketch by John McCarthy. The formalization is embedded in detailed literate style comments. We also briefly describe the Naproche approach.
Cite as

Adrian De Lon, Peter Koepke, and Anton Lorenzen. A Natural Formalization of the Mutilated Checkerboard Problem in Naproche. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{delon_et_al:LIPIcs.ITP.2021.16,
  author =	{De Lon, Adrian and Koepke, Peter and Lorenzen, Anton},
  title =	{{A Natural Formalization of the Mutilated Checkerboard Problem in Naproche}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{16:1--16:11},
  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.16},
  URN =		{urn:nbn:de:0030-drops-139112},
  doi =		{10.4230/LIPIcs.ITP.2021.16},
  annote =	{Keywords: checkerboard, formalization, formal mathematics, controlled language}
}
  • Refine by Type
  • 4 Document/PDF
  • 2 Document/HTML

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

  • Refine by Author
  • 2 Koepke, Peter
  • 1 Aberlé, C. B.
  • 1 Bhat, Siddharth
  • 1 Crary, Karl
  • 1 De Lon, Adrian
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Logic and verification
  • 1 Computing methodologies → Theorem proving algorithms
  • 1 Software and its engineering → Compilers
  • 1 Software and its engineering → Semantics
  • 1 Theory of computation → Rewrite systems
  • Show More...

  • Refine by Keyword
  • 2 formal mathematics
  • 2 formalization
  • 1 MLIR
  • 1 Naproche
  • 1 SSA
  • 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