Author name cluster

Benoît Valiron

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

CSL Conference 2025 Conference Paper

A Rewriting Theory for Quantum λ-Calculus

Claudia Faggian
Gaetan Lopez
Benoît Valiron

Quantum lambda calculus has been studied mainly as an idealized programming language - the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus are standardization and normalization results.

Details

FSCD Conference 2024 Conference Paper

Semantics for a Turing-Complete Reversible Programming Language with Inductive Types

Kostia Chardonnet
Louis Lemonnier
Benoît Valiron

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.

Details

CSL Conference 2023 Conference Paper

A Curry-Howard Correspondence for Linear, Reversible Computation

Kostia Chardonnet
Alexis Saurin
Benoît Valiron

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.

Details

MFCS Conference 2022 Conference Paper

LO_v-Calculus: A Graphical Language for Linear Optical Quantum Circuits

Alexandre Clément
Nicolas Heurtel
Shane Mansfield
Simon Perdrix
Benoît Valiron

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.

Details

MFCS Conference 2021 Conference Paper

Geometry of Interaction for ZX-Diagrams

Kostia Chardonnet
Benoît Valiron
Renaud Vilmart

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.

Details

I&C Journal 2017 Journal Article

The vectorial λ-calculus

Pablo Arrighi
Alejandro Díaz-Caro
Benoît Valiron

We describe a type system for the linear-algebraic λ-calculus. The type system accounts for the linear-algebraic aspects of this extension of λ-calculus: it is able to statically describe the linear combinations of terms that will be obtained when reducing the programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We prove that the resulting typed λ-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.

Details DOI