The following pages link to Benjamin Grégoire (Q633301):
Displaying 26 items.
- Certifying compilers using higher-order theorem provers as certificate checkers (Q633302) (← links)
- Masking the GLP lattice-based signature scheme at any order (Q1648842) (← links)
- An assertion-based program logic for probabilistic programs (Q2323970) (← links)
- Verified Indifferentiable Hashing into Elliptic Curves (Q2894324) (← links)
- Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs (Q2908554) (← links)
- Computer-Aided Cryptographic Proofs (Q2914729) (← links)
- Verified Proofs of Higher-Order Masking (Q2948340) (← links)
- A compiled implementation of strong reduction (Q2949209) (← links)
- Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving (Q3003228) (← links)
- Beyond Provable Security Verifiable IND-CCA Security of OAEP (Q3073706) (← links)
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses (Q3100209) (← links)
- Vectorizing Higher-Order Masking (Q3297549) (← links)
- Hardware Private Circuits: From Trivial Composition to Full Verification (Q3390006) (← links)
- A Computational Approach to Pocklington Certificates in Type Theory (Q3434628) (← links)
- Relational Reasoning via Probabilistic Coupling (Q3460069) (← links)
- Type-Based Termination with Sized Products (Q3540199) (← links)
- Preservation of Proof Obligations from Java to the Java Virtual Machine (Q3541689) (← links)
- Certificate Translation for Optimizing Compilers (Q3613391) (← links)
- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers (Q3613425) (← links)
- Formal Certification of ElGamal Encryption (Q3619468) (← links)
- A New Elimination Rule for the Calculus of Inductive Constructions (Q3638245) (← links)
- (Q4598248) (← links)
- Proving Differential Privacy via Probabilistic Couplings (Q4635938) (← links)
- Proving uniformity and independence by self-composition and coupling (Q4645748) (← links)
- On Strong Normalization of the Calculus of Constructions with Type-Based Termination (Q4933315) (← links)
- Masking the GLP lattice-based signature scheme at any order (Q6182002) (← links)
