DROPS

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.CSL.2021.19

Realizability with Stateful Computations for Nonstandard Analysis

Authors: Bruno Dinis and Étienne Miquey

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract

In this paper we propose a new approach to realizability interpretations for nonstandard arithmetic. We deal with nonstandard analysis in the context of intuitionistic realizability, focusing on the Lightstone-Robinson construction of a model for nonstandard analysis through an ultrapower. In particular, we consider an extension of the λ-calculus with a memory cell, that contains an integer (the state), in order to indicate in which slice of the ultrapower ℳ^{ℕ} the computation is being done. We shall pay attention to the nonstandard principles (and their computational content) obtainable in this setting. We then discuss how this product could be quotiented to mimic the Lightstone-Robinson construction.

Cite as

Bruno Dinis and Étienne Miquey. Realizability with Stateful Computations for Nonstandard Analysis. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dinis_et_al:LIPIcs.CSL.2021.19,
  author =	{Dinis, Bruno and Miquey, \'{E}tienne},
  title =	{{Realizability with Stateful Computations for Nonstandard Analysis}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{19:1--19:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.19},
  URN =		{urn:nbn:de:0030-drops-134531},
  doi =		{10.4230/LIPIcs.CSL.2021.19},
  annote =	{Keywords: realizability, nonstandard analysis, states, glueing, ultrafilters, {\L}o\'{s}' theorem}
}

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}
}

4 Search Results for "Blot, Valentin"

A Semantics of 𝕂 into Dedukti

Abstract

Cite as

Diller-Nahm Bar Recursion

Abstract

Cite as

Realizability with Stateful Computations for Nonstandard Analysis

Abstract

Cite as

Classical Extraction in Continuation Models

Abstract

Cite as

Thanks for your feedback!

Could not send message