3 Search Results for "Chardonnet, Kostia"

Document
DOI: 10.4230/LIPIcs.CSL.2023.13
A Curry-Howard Correspondence for Linear, Reversible Computation

Authors: Kostia Chardonnet, Alexis Saurin, and Benoît Valiron

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic μMALL: linear logic extended with least fixed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy μMALL validity criterion and how the language simulates the cut-elimination procedure of μMALL.
Cite as

Kostia Chardonnet, Alexis Saurin, and Benoît Valiron. A Curry-Howard Correspondence for Linear, Reversible Computation. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chardonnet_et_al:LIPIcs.CSL.2023.13,
  author =	{Chardonnet, Kostia and Saurin, Alexis and Valiron, Beno\^{i}t},
  title =	{{A Curry-Howard Correspondence for Linear, Reversible Computation}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.13},
  URN =		{urn:nbn:de:0030-drops-174747},
  doi =		{10.4230/LIPIcs.CSL.2023.13},
  annote =	{Keywords: Reversible Computation, Linear Logic, Curry-Howard}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.30
Geometry of Interaction for ZX-Diagrams

Authors: Kostia Chardonnet, Benoît Valiron, and Renaud Vilmart

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
ZX-Calculus is a versatile graphical language for quantum computation equipped with an equational theory. Getting inspiration from Geometry of Interaction, in this paper we propose a token-machine-based asynchronous model of both pure ZX-Calculus and its extension to mixed processes. We also show how to connect this new semantics to the usual standard interpretation of ZX-diagrams. This model allows us to have a new look at what ZX-diagrams compute, and give a more local, operational view of the semantics of ZX-diagrams.
Cite as

Kostia Chardonnet, Benoît Valiron, and Renaud Vilmart. Geometry of Interaction for ZX-Diagrams. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{chardonnet_et_al:LIPIcs.MFCS.2021.30,
  author =	{Chardonnet, Kostia and Valiron, Beno\^{i}t and Vilmart, Renaud},
  title =	{{Geometry of Interaction for ZX-Diagrams}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.30},
  URN =		{urn:nbn:de:0030-drops-144701},
  doi =		{10.4230/LIPIcs.MFCS.2021.30},
  annote =	{Keywords: Quantum Computation, Linear Logic, ZX-Calculus, Geometry of Interaction}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.31
Encoding Agda Programs Using Rewriting

Authors: Guillaume Genestier

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
We present in this paper an encoding in an extension with rewriting of the Edimburgh Logical Framework (LF) [Harper et al., 1993] of two common features: universe polymorphism and eta-convertibility. This encoding is at the root of the translator between Agda and Dedukti developped by the author.
Cite as

Guillaume Genestier. Encoding Agda Programs Using Rewriting. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{genestier:LIPIcs.FSCD.2020.31,
  author =	{Genestier, Guillaume},
  title =	{{Encoding Agda Programs Using Rewriting}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{31:1--31:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.31},
  URN =		{urn:nbn:de:0030-drops-123530},
  doi =		{10.4230/LIPIcs.FSCD.2020.31},
  annote =	{Keywords: Logical Frameworks, Rewriting, Universe Polymorphism, Eta Conversion}
}
  • Refine by Author
  • 2 Chardonnet, Kostia
  • 2 Valiron, Benoît
  • 1 Genestier, Guillaume
  • 1 Saurin, Alexis
  • 1 Vilmart, Renaud

  • Refine by Classification
  • 3 Theory of computation → Equational logic and rewriting
  • 2 Theory of computation → Linear logic
  • 1 Theory of computation → Quantum computation theory
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 2 Linear Logic
  • 1 Curry-Howard
  • 1 Eta Conversion
  • 1 Geometry of Interaction
  • 1 Logical Frameworks
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 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