4 Search Results for "van Doorn, Floris"

Document
DOI: 10.4230/LIPIcs.ITP.2023.15
Closure Properties of General Grammars – Formally Verified

Authors: Martin Dvorak and Jasmin Blanchette

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

Abstract
We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.
Cite as

Martin Dvorak and Jasmin Blanchette. Closure Properties of General Grammars – Formally Verified. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dvorak_et_al:LIPIcs.ITP.2023.15,
  author =	{Dvorak, Martin and Blanchette, Jasmin},
  title =	{{Closure Properties of General Grammars – Formally Verified}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{15:1--15:16},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15},
  URN =		{urn:nbn:de:0030-drops-183906},
  doi =		{10.4230/LIPIcs.ITP.2023.15},
  annote =	{Keywords: Lean, type-0 grammars, recursively enumerable languages, Kleene star}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.18
Formalized Haar Measure

Authors: Floris van Doorn

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

Abstract
We describe the formalization of the existence and uniqueness of the Haar measure in the Lean theorem prover. The Haar measure is an invariant regular measure on locally compact groups, and it has not been formalized in a proof assistant before. We will also discuss the measure theory library in Lean’s mathematical library mathlib, and discuss the construction of product measures and the proof of Fubini’s theorem for the Bochner integral.
Cite as

Floris van Doorn. Formalized Haar Measure. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{vandoorn:LIPIcs.ITP.2021.18,
  author =	{van Doorn, Floris},
  title =	{{Formalized Haar Measure}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{18:1--18:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.18},
  URN =		{urn:nbn:de:0030-drops-139139},
  doi =		{10.4230/LIPIcs.ITP.2021.18},
  annote =	{Keywords: Haar measure, measure theory, Bochner integral, Lean, interactive theorem proving, formalized mathematics}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2019.8
Coherence for Monoidal Groupoids in HoTT

Authors: Stefano Piceghello

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Abstract
We present a proof of coherence for monoidal groupoids in homotopy type theory. An important role in the formulation and in the proof of coherence is played by groupoids with a free monoidal structure; these can be represented by 1-truncated higher inductive types, with constructors freely generating their defining objects, natural isomorphisms and commutative diagrams. All results included in this paper have been formalised in the proof assistant Coq.
Cite as

Stefano Piceghello. Coherence for Monoidal Groupoids in HoTT. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{piceghello:LIPIcs.TYPES.2019.8,
  author =	{Piceghello, Stefano},
  title =	{{Coherence for Monoidal Groupoids in HoTT}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.8},
  URN =		{urn:nbn:de:0030-drops-130722},
  doi =		{10.4230/LIPIcs.TYPES.2019.8},
  annote =	{Keywords: homotopy type theory, coherence, monoidal categories, groupoids, higher inductive types, formalisation, Coq}
}
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-dev.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 Author
  • 2 van Doorn, Floris
  • 1 Blanchette, Jasmin
  • 1 Dvorak, Martin
  • 1 Han, Jesse Michael
  • 1 Piceghello, Stefano

  • Refine by Classification
  • 3 Theory of computation → Type theory
  • 1 Mathematics of computing → Mathematical analysis
  • 1 Software and its engineering → Formal methods
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 3 Lean
  • 1 Bochner integral
  • 1 Boolean-valued models
  • 1 Coq
  • 1 Haar measure
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2019
  • 1 2020
  • 1 2021
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact