2 papers
cs.LO2023
A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful prog…
cs.PL2023
Typed compositional quantum computation with lenses
Jacques Garrigue, Takafumi Saikawa
We propose a type-theoretic framework for describing and proving properties of quantum computations, in particular those presented as quantum circuits. Our proposal is based on an…