4 Search Results for "Hudon, Simon"

Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2025.37
LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper)

Authors: Eric Vin, Kyle A. Miller, and Daniel J. Fremont

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

Abstract
We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, making it straightforward to define properties involving numerical or other types. We prove that standard flavors of LTL can be embedded in our framework. The library also provides automation for reasoning about LeanLTL formulas in a way that facilitates using Lean’s existing tactics. Finally, we provide examples illustrating the utility of the library in reasoning about systems that come from applications.
Cite as

Eric Vin, Kyle A. Miller, and Daniel J. Fremont. LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 37:1-37:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vin_et_al:LIPIcs.ITP.2025.37,
  author =	{Vin, Eric and Miller, Kyle A. and Fremont, Daniel J.},
  title =	{{LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{37:1--37:9},
  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.37},
  URN =		{urn:nbn:de:0030-drops-246356},
  doi =		{10.4230/LIPIcs.ITP.2025.37},
  annote =	{Keywords: Linear Temporal Logic, Interactive Theorem Proving, Lean 4}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.27
Teaching Mathematics Using Lean and Controlled Natural Language

Authors: Patrick Massot

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

Abstract
We present Verbose Lean, a library using the flexibility of the Lean programming language and proof assistant to teach undergrad mathematics students how to read and write traditional paper proofs. After explaining our main pedagogical goals, we explain how students use the library with varying levels of assistance to write proofs that are easy to transfer to paper because they look like natural language. We then describe how teachers can customize the student experience based on their specific pedagogical goals and constraints. Finally we describe some aspects of the implementation of the library, emphasizing how new aspects of the very recently released version 4 of Lean allow a lot of flexibility that could benefit many new creative uses of a proof assistant.
Cite as

Patrick Massot. Teaching Mathematics Using Lean and Controlled Natural Language. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{massot:LIPIcs.ITP.2024.27,
  author =	{Massot, Patrick},
  title =	{{Teaching Mathematics Using Lean and Controlled Natural Language}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{27:1--27:19},
  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.27},
  URN =		{urn:nbn:de:0030-drops-207550},
  doi =		{10.4230/LIPIcs.ITP.2024.27},
  annote =	{Keywords: mathematics teaching, proof assistant, controlled natural language}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.6
Data Types as Quotients of Polynomial Functors

Authors: Jeremy Avigad, Mario Carneiro, and Simon Hudon

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
A broad class of data types, including arbitrary nestings of inductive types, coinductive types, and quotients, can be represented as quotients of polynomial functors. This provides perspicuous ways of constructing them and reasoning about them in an interactive theorem prover.
Cite as

Jeremy Avigad, Mario Carneiro, and Simon Hudon. Data Types as Quotients of Polynomial Functors. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{avigad_et_al:LIPIcs.ITP.2019.6,
  author =	{Avigad, Jeremy and Carneiro, Mario and Hudon, Simon},
  title =	{{Data Types as Quotients of Polynomial Functors}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.6},
  URN =		{urn:nbn:de:0030-drops-110612},
  doi =		{10.4230/LIPIcs.ITP.2019.6},
  annote =	{Keywords: data types, polynomial functors, inductive types, coinductive types}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.19
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis

Authors: Jesse Michael Han and Floris van Doorn

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space 2^{omega_2 x omega} and formally verify the failure of the continuum hypothesis in the resulting model.
Cite as

Jesse Michael Han and Floris van Doorn. A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{han_et_al:LIPIcs.ITP.2019.19,
  author =	{Han, Jesse Michael and van Doorn, Floris},
  title =	{{A Formalization of Forcing and the Unprovability of the Continuum Hypothesis}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.19},
  URN =		{urn:nbn:de:0030-drops-110742},
  doi =		{10.4230/LIPIcs.ITP.2019.19},
  annote =	{Keywords: Interactive theorem proving, formal verification, set theory, forcing, independence proofs, continuum hypothesis, Boolean-valued models, Lean}
}
  • Refine by Type
  • 4 Document/PDF
  • 1 Document/HTML

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

  • Refine by Author
  • 1 Avigad, Jeremy
  • 1 Carneiro, Mario
  • 1 Fremont, Daniel J.
  • 1 Han, Jesse Michael
  • 1 Hudon, Simon
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs

  • Refine by Classification
  • 4 Theory of computation → Logic and verification
  • 3 Theory of computation → Type theory
  • 1 Applied computing → Interactive learning environments
  • 1 Human-centered computing → Natural language interfaces
  • 1 Software and its engineering → Formal methods
  • Show More...

  • Refine by Keyword
  • 1 Boolean-valued models
  • 1 Interactive Theorem Proving
  • 1 Interactive theorem proving
  • 1 Lean
  • 1 Lean 4
  • 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact