3 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…
cs.LO2020
Formal Adventures in Convex and Conical Spaces
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
Convex sets appear in various mathematical theories, and are used to define notions such as convex functions and hulls. As an abstraction from the usual definition of convex sets i…