| Publication | Date of Publication | Type |
|---|
Formally verifying Kyber. Episode V: machine-checked IND-CCA security and correctness of ML-KEM in Easycrypt
| 2024-12-04 | Paper |
Machine-checked security for XMSS as in RFC 8391 and SPHINCS\textsuperscript{+}
Advances in Cryptology – CRYPTO 2023 | 2024-02-06 | Paper |
scientific article; zbMATH DE number 7699425 (Why is no real title available?)
| 2023-06-20 | Paper |
Formal verification of Saber's public-key encryption scheme in easycrypt
Advances in Cryptology – CRYPTO 2022 | 2023-06-12 | Paper |
Formalizing the Face Lattice of Polyhedra
Automated Reasoning | 2022-11-09 | Paper |
Formalizing the face lattice of polyhedra
| 2022-08-02 | Paper |
Formalizing the Face Lattice of Polyhedra
| 2021-04-30 | Paper |
\(*\)-liftings for differential privacy
| 2020-05-27 | Paper |
scientific article; zbMATH DE number 7178368 (Why is no real title available?)
| 2020-03-09 | Paper |
Relational \(\star\)-liftings for differential privacy
| 2020-01-03 | Paper |
An assertion-based program logic for probabilistic programs
| 2019-09-13 | Paper |
Theory of types and decision procedures
| 2019-02-15 | Paper |
Coq without type casts: a complete proof of Coq Modulo Theory
EPiC Series in Computing | 2019-01-10 | Paper |
Proving uniformity and independence by self-composition and coupling
EPiC Series in Computing | 2019-01-10 | Paper |
Proving differential privacy via probabilistic couplings
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
scientific article; zbMATH DE number 6820296 (Why is no real title available?)
| 2017-12-19 | Paper |
Coupling proofs are probabilistic product programs
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | Paper |
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model
Lecture Notes in Computer Science | 2017-06-13 | Paper |
Computer-aided verification for mechanism design
Web and Internet Economics | 2017-02-10 | Paper |
Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-10-24 | Paper |
Higher-order approximate relational refinement types for mechanism design and differential privacy
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-09-29 | Paper |
Relational reasoning via probabilistic coupling
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Verified Proofs of Higher-Order Masking
Advances in Cryptology -- EUROCRYPT 2015 | 2015-09-30 | Paper |
Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
EasyCrypt: a tutorial
Foundations of Security Analysis and Design VII | 2015-05-27 | Paper |
Secure distributed programming with value-dependent types
Proceedings of the 16th ACM SIGPLAN international conference on Functional programming | 2015-03-05 | Paper |
Fully abstract compilation to JavaScript
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-11-27 | Paper |
A formal library for elliptic curves in the Coq proof assistant
Interactive Theorem Proving | 2014-09-08 | Paper |
Proving the TLS handshake secure (as it is)
Advances in Cryptology – CRYPTO 2014 | 2014-08-07 | Paper |
Gradual typing embedded securely in JavaScript
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Probabilistic relational verification for cryptographic implementations
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Secure distributed programming with value-dependent types
Journal of Functional Programming | 2014-02-27 | Paper |
Coq Modulo Theory
Computer Science Logic | 2010-09-03 | Paper |
Building Decision Procedures in the Calculus of Inductive Constructions
Computer Science Logic | 2009-03-05 | Paper |
