2 Search Results for "Monin, Jean-François"

Document
DOI: 10.4230/LIPIcs.ITP.2023.21
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq

Authors: Dominique Larchey-Wendling and Jean-François Monin

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

Abstract
Basing on an original Coq implementation of unbounded linear search for partially decidable predicates, we study the computational contents of μ-recursive functions via their syntactic representation, and a correct by construction Coq interpreter for this abstract syntax. When this interpreter is extracted, we claim the resulting OCaml code to be the natural combination of the implementation of the μ-recursive schemes of composition, primitive recursion and unbounded minimization of partial (i.e., possibly non-terminating) functions. At the level of the fully specified Coq terms, this implies the representation of higher-order functions of which some of the arguments are themselves partial functions. We handle this issue using some techniques coming from the Braga method. Hence we get a faithful embedding of μ-recursive algorithms into Coq preserving not only their extensional meaning but also their intended computational behavior. We put a strong focus on the quality of the Coq artifact which is both self contained and with a line of code count of less than 1k in total.
Cite as

Dominique Larchey-Wendling and Jean-François Monin. Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 21:1-21:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{larcheywendling_et_al:LIPIcs.ITP.2023.21,
  author =	{Larchey-Wendling, Dominique and Monin, Jean-Fran\c{c}ois},
  title =	{{Proof Pearl: Faithful Computation and Extraction of \mu-Recursive Algorithms in Coq}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{21:1--21:17},
  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.21},
  URN =		{urn:nbn:de:0030-drops-183963},
  doi =		{10.4230/LIPIcs.ITP.2023.21},
  annote =	{Keywords: Unbounded linear search, \mu-recursive functions, computational contents, Coq, extraction, OCaml}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.34
Another Characterization of the Higher K-Trivials

Authors: Paul-Elliot Anglès d'Auriac and Benoit Monin

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
In algorithmic randomness, the class of K-trivial sets has proved itself to be remarkable, due to its numerous different characterizations. We pursue in this paper some work already initiated on K-trivials in the context of higher randomness. In particular we give here another characterization of the non hyperarithmetic higher K-trivial sets.
Cite as

Paul-Elliot Anglès d'Auriac and Benoit Monin. Another Characterization of the Higher K-Trivials. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 34:1-34:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{anglesdauriac_et_al:LIPIcs.MFCS.2017.34,
  author =	{Angl\`{e}s d'Auriac, Paul-Elliot and Monin, Benoit},
  title =	{{Another Characterization of the Higher K-Trivials}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{34:1--34:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.34},
  URN =		{urn:nbn:de:0030-drops-80837},
  doi =		{10.4230/LIPIcs.MFCS.2017.34},
  annote =	{Keywords: Algorithmic randomness, higher computability, K-triviality, effective descriptive set theory, Kolmogorov complexity}
}
  • Refine by Author
  • 1 Anglès d'Auriac, Paul-Elliot
  • 1 Larchey-Wendling, Dominique
  • 1 Monin, Benoit
  • 1 Monin, Jean-François

  • Refine by Classification
  • 1 Software and its engineering → Formal methods
  • 1 Software and its engineering → Functional languages
  • 1 Theory of computation → Functional constructs
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Models of computation
  • Show More...

  • Refine by Keyword
  • 1 Algorithmic randomness
  • 1 Coq
  • 1 K-triviality
  • 1 Kolmogorov complexity
  • 1 OCaml
  • Show More...

  • Refine by Type
  • 2 document

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