Search Results

Documents authored by Valiron, Benoît

Document
DOI: 10.4230/LIPIcs.FSCD.2024.19
Semantics for a Turing-Complete Reversible Programming Language with Inductive Types

Authors: Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, pattern-matching is used to ensure the reversibility of functions. We show how one can encode any Reversible Turing Machine in said language. We then build a sound and adequate categorical semantics based on join inverse categories, with additional structures to capture pattern-matching and to interpret inductive types and recursion. We then derive a notion of completeness in the sense that any computable, partial, first-order injective function is the image of a term in the language.
Cite as

Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron. Semantics for a Turing-Complete Reversible Programming Language with Inductive Types. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chardonnet_et_al:LIPIcs.FSCD.2024.19,
  author =	{Chardonnet, Kostia and Lemonnier, Louis and Valiron, Beno\^{i}t},
  title =	{{Semantics for a Turing-Complete Reversible Programming Language with Inductive Types}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.19},
  URN =		{urn:nbn:de:0030-drops-203487},
  doi =		{10.4230/LIPIcs.FSCD.2024.19},
  annote =	{Keywords: Reversible programming, functional programming, Computability, Denotational Semantics}
}
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.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.2022.35
LO_v-Calculus: A Graphical Language for Linear Optical Quantum Circuits

Authors: Alexandre Clément, Nicolas Heurtel, Shane Mansfield, Simon Perdrix, and Benoît Valiron

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We introduce the LO_v-calculus, a graphical language for reasoning about linear optical quantum circuits with so-called vacuum state auxiliary inputs. We present the axiomatics of the language and prove its soundness and completeness: two LO_v-circuits represent the same quantum process if and only if one can be transformed into the other with the rules of the LO_v-calculus. We give a confluent and terminating rewrite system to rewrite any polarisation-preserving LO_v-circuit into a unique triangular normal form, inspired by the universal decomposition of Reck et al. (1994) for linear optical quantum circuits.
Cite as

Alexandre Clément, Nicolas Heurtel, Shane Mansfield, Simon Perdrix, and Benoît Valiron. LO_v-Calculus: A Graphical Language for Linear Optical Quantum Circuits. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{clement_et_al:LIPIcs.MFCS.2022.35,
  author =	{Cl\'{e}ment, Alexandre and Heurtel, Nicolas and Mansfield, Shane and Perdrix, Simon and Valiron, Beno\^{i}t},
  title =	{{LO\underlinev-Calculus: A Graphical Language for Linear Optical Quantum Circuits}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{35:1--35:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.35},
  URN =		{urn:nbn:de:0030-drops-168334},
  doi =		{10.4230/LIPIcs.MFCS.2022.35},
  annote =	{Keywords: Quantum Computing, Graphical Language, Linear Optical Circuits, Linear Optical Quantum Computing, Completeness}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2021.51
Concrete Categorical Model of a Quantum Circuit Description Language with Measurement

Authors: Dongho Lee, Valentin Perrelle, Benoît Valiron, and Zhaowei Xu

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
In this paper, we introduce dynamic lifting to a quantum circuit-description language, following the Proto-Quipper language approach. Dynamic lifting allows programs to transfer the result of measuring quantum data - qubits - into classical data - booleans -. We propose a type system and an operational semantics for the language and we state safety properties. Next, we introduce a concrete categorical semantics for the proposed language, basing our approach on a recent model from Rios&Selinger for Proto-Quipper-M. Our approach is to construct on top of a concrete category of circuits with measurements a Kleisli category, capturing as a side effect the action of retrieving classical content out of a quantum memory. We then show a soundness result for this semantics.
Cite as

Dongho Lee, Valentin Perrelle, Benoît Valiron, and Zhaowei Xu. Concrete Categorical Model of a Quantum Circuit Description Language with Measurement. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 51:1-51:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{lee_et_al:LIPIcs.FSTTCS.2021.51,
  author =	{Lee, Dongho and Perrelle, Valentin and Valiron, Beno\^{i}t and Xu, Zhaowei},
  title =	{{Concrete Categorical Model of a Quantum Circuit Description Language with Measurement}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{51:1--51:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.51},
  URN =		{urn:nbn:de:0030-drops-155627},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.51},
  annote =	{Keywords: Categorical semantics, Operational semantics, Quantum circuit description language}
}
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.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}
}
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