3 papers
cs.LO2025
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…
cs.LO2025
The Many-Worlds Calculus
Kostia Chardonnet, Marc de Visme, Benoît Valiron +1
In this paper, we explore the interaction between two monoidal structures: a multiplicative one, for the encoding of pairing, and an additive one, for the encoding of choice. We pr…
cs.LO2025
A Rewriting Theory for Quantum Lambda-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…