Search Results

Documents authored by Blot, Valentin

Document
DOI: 10.4230/LIPIcs.TYPES.2022.12
A Semantics of 𝕂 into Dedukti

Authors: Amélie Ledein, Valentin Blot, and Catherine Dubois

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
𝕂 is a semantical framework for formally describing the semantics of programming languages thanks to a BNF grammar and rewriting rules on configurations. It is also an environment that offers various tools to help programming with the languages specified in the formalism. For example, it is possible to execute programs thanks to the generated interpreter, or to check their properties thanks to the provided automatic theorem prover called the KProver. 𝕂 is based on la Matching Logic, a first-order logic with an application and fixed-point operators, extended with symbols to encode equality, typing and rewriting. This specific la Matching Logic theory is called Kore. Dedukti is a logical framework having for main goal the interoperability of proofs between different formal proof tools. Several translators to Dedukti exist or are under development, in order to automatically translate formalizations written, for instance, in Coq or PVS. Dedukti is based on the λΠ-calculus modulo theory, a λ-calculus with dependent types and extended with a primitive notion of computation defined by rewriting rules. The flexibility of this logical framework allows to encode many theories ranging from first-order logic to the Calculus of Constructions. In this article, we present a paper formalization of the translation from 𝕂 into Kore, and a paper formalization and an automatic translation tool, called KaMeLo, from Kore to Dedukti in order to execute programs in Dedukti.
Cite as

Amélie Ledein, Valentin Blot, and Catherine Dubois. A Semantics of 𝕂 into Dedukti. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ledein_et_al:LIPIcs.TYPES.2022.12,
  author =	{Ledein, Am\'{e}lie and Blot, Valentin and Dubois, Catherine},
  title =	{{A Semantics of \mathbb{K} into Dedukti}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{12:1--12:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.12},
  URN =		{urn:nbn:de:0030-drops-184557},
  doi =		{10.4230/LIPIcs.TYPES.2022.12},
  annote =	{Keywords: Programming language, Semantics, Rewriting, Logical framework, Type theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.32
Diller-Nahm Bar Recursion

Authors: Valentin Blot

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

Abstract
We present a generalization of Spector’s bar recursion to the Diller-Nahm variant of Gödel’s Dialectica interpretation. This generalized bar recursion collects witnesses of universal formulas in sets of approximation sequences to provide an interpretation to the double-negation shift principle. The interpretation is presented in a fully computational way, implementing sets via lists. We also present a demand-driven version of this extended bar recursion manipulating partial sequences rather than initial segments. We explain why in a Diller-Nahm context there seems to be several versions of this demand-driven bar recursion, but no canonical one.
Cite as

Valentin Blot. Diller-Nahm Bar Recursion. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{blot:LIPIcs.FSCD.2023.32,
  author =	{Blot, Valentin},
  title =	{{Diller-Nahm Bar Recursion}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{32:1--32:16},
  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.32},
  URN =		{urn:nbn:de:0030-drops-180164},
  doi =		{10.4230/LIPIcs.FSCD.2023.32},
  annote =	{Keywords: Dialectica, Bar recursion}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.13
Classical Extraction in Continuation Models

Authors: Valentin Blot

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
We use the control features of continuation models to interpret proofs in first-order classical theories. This interpretation is suitable for extracting algorithms from proofs of Pi^0_2 formulas. It is fundamentally different from the usual direct interpretation, which is shown to be equivalent to Friedman's trick. The main difference is that atomic formulas and natural numbers are interpreted as distinct objects. Nevertheless, the control features inherent to the continuation models permit extraction using a special "channel" on which the extracted value is transmitted at toplevel without unfolding the recursive calls. We prove that the technique fails in Scott domains, but succeeds in the refined setting of Laird's bistable bicpos, as well as in game semantics.
Cite as

Valentin Blot. Classical Extraction in Continuation Models. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{blot:LIPIcs.FSCD.2016.13,
  author =	{Blot, Valentin},
  title =	{{Classical Extraction in Continuation Models}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.13},
  URN =		{urn:nbn:de:0030-drops-59913},
  doi =		{10.4230/LIPIcs.FSCD.2016.13},
  annote =	{Keywords: Extraction, Classical Logic, Control Operators, Game Semantics}
}
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