98 citations · 437 across the 19 of their papers we have counts for
22 papers
ShannonProver: Towards Automating Formal Cryptographic Proofs
Yiping Ma, Yu-Lin Tsai, Mayank Rathee +4
Cryptographic proofs are produced at a scale that increasingly exceeds the community's ability to verify them manually. Machine-checked proofs offer a path toward scalable proof ve…
A drag-and-drop proof tactic
Pablo Donato, Pierre-Yves Strub, Benjamin Werner
We explore the features of a user interface where formal proofs can be built through gestural actions. In particular, we show how proof construction steps can be associated to drag…
CoqQ: Foundational Verification of Quantum Programs
Li Zhou, Gilles Barthe, Pierre-Yves Strub +2
CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quant…
Formalizing the Face Lattice of Polyhedra
Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub
Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistan…
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe +5
We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected ag…
Computer-aided proofs for multiparty computation with active security
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner +2
Secure multi-party computation (MPC) is a general cryptographic technique that allows distrusting parties to compute a function of their individual inputs, while only revealing the…