2 Search Results for "Kerjean, Marie"

Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2023.36
Fermat’s Last Theorem for Regular Primes (Short Paper)

Authors: Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi

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

Abstract
We formalise the proof of the first case of Fermat’s Last Theorem for regular primes using the Lean theorem prover and its mathematical library mathlib. This is an important 19th century result that motivated the development of modern algebraic number theory. Besides explaining the mathematics behind this result, we analyze in this paper the difficulties we faced in the formalisation process and how we solved them. For example, we had to deal with a diamond about characteristic zero fields and problems arising from multiple nested coercions related to number fields. We also explain how we integrated our work to mathlib.
Cite as

Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi. Fermat’s Last Theorem for Regular Primes (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 36:1-36:8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{best_et_al:LIPIcs.ITP.2023.36,
  author =	{Best, Alex J. and Birkbeck, Christopher and Brasca, Riccardo and Rodriguez Boidi, Eric},
  title =	{{Fermat’s Last Theorem for Regular Primes}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{36:1--36:8},
  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.36},
  URN =		{urn:nbn:de:0030-drops-184115},
  doi =		{10.4230/LIPIcs.ITP.2023.36},
  annote =	{Keywords: Fermat’s Last Theorem, Cyclotomic fields, Interactive theorem proving, Lean}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.21
Unifying Graded Linear Logic and Differential Operators

Authors: Flavien Breuvart, Marie Kerjean, and Simon Mirwasser

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
Linear Logic refines Classical Logic by taking into account the resources used during the proof and program computation. In the past decades, it has been extended to various frameworks. The most famous are indexed linear logics which can describe the resource management or the complexity analysis of a program. From another perspective, Differential Linear Logic is an extension which allows the linearization of proofs. In this article, we merge these two directions by first defining a differential version of Graded linear logic: this is made by indexing exponential connectives with a monoid of differential operators. We prove that it is equivalent to a graded version of previously defined extension of finitary differential linear logic. We give a denotational model of our logic, based on distribution theory and linear partial differential operators with constant coefficients.
Cite as

Flavien Breuvart, Marie Kerjean, and Simon Mirwasser. Unifying Graded Linear Logic and Differential Operators. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 21:1-21:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{breuvart_et_al:LIPIcs.FSCD.2023.21,
  author =	{Breuvart, Flavien and Kerjean, Marie and Mirwasser, Simon},
  title =	{{Unifying Graded Linear Logic and Differential Operators}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.21},
  URN =		{urn:nbn:de:0030-drops-180052},
  doi =		{10.4230/LIPIcs.FSCD.2023.21},
  annote =	{Keywords: Linear Logic, Denotational Semantics, Functional Analysis, Graded Logic}
}
  • Refine by Author
  • 1 Best, Alex J.
  • 1 Birkbeck, Christopher
  • 1 Brasca, Riccardo
  • 1 Breuvart, Flavien
  • 1 Kerjean, Marie
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Representation of mathematical objects
  • 1 General and reference → Verification
  • 1 Mathematics of computing → Mathematical software
  • 1 Mathematics of computing → Partial differential equations
  • 1 Theory of computation → Denotational semantics
  • Show More...

  • Refine by Keyword
  • 1 Cyclotomic fields
  • 1 Denotational Semantics
  • 1 Fermat’s Last Theorem
  • 1 Functional Analysis
  • 1 Graded Logic
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 2 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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact