12 citations · 19 across the 6 of their papers we have counts for
9 papers
Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
Son Ho, Cédric Fournet, Jonathan Protzenko +7
We develop a new methodology for verifying cryptographic software. We target production code written in Rust for performance and system integration, rather than verification conven…
Charon: An Analysis Framework for Rust
Son Ho, Guillaume Boisseau, Lucas Franceschino +3
With the explosion in popularity of the Rust programming language, a wealth of tools have recently been developed to analyze, verify, and test Rust programs. Alas, the Rust ecosyst…
Cornering Optics
Guillaume Boisseau, Chad Nester, Mario Román
We show that the category of optics in a monoidal category arises naturally from the free cornering of that category. Further, we show that the free cornering of a monoidal categor…
Graphical Piecewise-Linear Algebra
Guillaume Boisseau, Robin Piedeleu
Graphical (Linear) Algebra is a family of diagrammatic languages allowing to reason about different kinds of subsets of vector spaces compositionally. It has been used to model var…
String Diagrammatic Electrical Circuit Theory
Guillaume Boisseau, Paweł Sobociński
We develop a comprehensive string diagrammatic treatment of electrical circuits. Building on previous, limited case studies, we introduce controlled sources and meters as elements,…
Diagrammatic Polyhedral Algebra
Filippo Bonchi, Alessandro Di Giorgio, Pawel Sobocinski
We extend the theory of Interacting Hopf algebras with an order primitive, and give a sound and complete axiomatisation of the prop of polyhedral cones. Next, we axiomatise an affi…
The Safari of Update Structures: Visiting the Lens and Quantum Enclosures
Matthew Wilson, James Hefford, Guillaume Boisseau +1
We build upon our recently introduced concept of an update structure to show that it is a generalisation of very-well-behaved lenses, that is, there is a bijection between a strict…
String Diagrams for Optics
Guillaume Boisseau
Optics are a data representation for compositional data access, with lenses as a popular special case. Hedges has presented a diagrammatic calculus for lenses, but in a way that do…
Understanding Profunctor Optics: a representation theorem
Guillaume Boisseau
Optics, aka functional references, are classes of tools that allow composable access into compound data structures. Usually defined as programming language libraries, they provide…