The following pages link to Gilles Barthe (Q236461):
Displaying 50 items.
- Tool-assisted specification and verification of typed low-level languages (Q861687) (← links)
- Security types preserving compilation (Q865705) (← links)
- CPS translations and applications: The cube and beyond (Q1125574) (← links)
- Order-sorted inductive types (Q1286367) (← links)
- Masking the GLP lattice-based signature scheme at any order (Q1648842) (← links)
- Generic transformations of predicate encodings: constructions and applications (Q1675716) (← links)
- System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory (Q2228439) (← links)
- An assertion-based program logic for probabilistic programs (Q2323970) (← links)
- Relational reasoning for Markov chains in a probabilistic guarded lambda calculus (Q2323974) (← links)
- Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs (Q2331068) (← links)
- Product programs and relational program logics (Q2374302) (← links)
- System-level non-interference of constant-time cryptography. I: Model (Q2417947) (← links)
- Automated analysis of cryptographic assumptions in generic group models (Q2423840) (← links)
- A formal treatment of the role of verified compilers in secure computation (Q2669248) (← links)
- (Q2763680) (← links)
- (Q2766771) (← links)
- (Q2767030) (← links)
- (Q2769425) (← links)
- Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy (Q2819789) (← links)
- Automated Analysis of Cryptographic Assumptions in Generic Group Models (Q2874498) (← links)
- A Computational Indistinguishability Logic for the Bounded Storage Model (Q2889822) (← 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)
- Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds (Q2941200) (← links)
- Probabilistic relational reasoning for differential privacy (Q2942860) (← links)
- Pure patterns type systems (Q2942930) (← links)
- Verified Proofs of Higher-Order Masking (Q2948340) (← links)
- Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols (Q2948400) (← links)
- Computer-Aided Verification for Mechanism Design (Q2959836) (← links)
- Formally Verified Implementation of an Idealized Model of Virtualization (Q2968409) (← links)
- Is Your Software on Dope? (Q2988635) (← links)
- (Q3024819) (← links)
- On the Equality of Probabilistic Terms (Q3066090) (← links)
- Beyond Provable Security Verifiable IND-CCA Security of OAEP (Q3073706) (← links)
- Verifiable Security of Boneh-Franklin Identity-Based Encryption (Q3092349) (← links)
- Secure information flow by self-composition (Q3103613) (← links)
- An Introduction to Certificate Translation (Q3184785) (← links)
- A computational view of implicit coercions in type theory (Q3372684) (← links)
- Remarks on the equational theory of non-normalizing pure type systems (Q3377459) (← links)
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant (Q3434629) (← links)
- Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification (Q3455833) (← links)
- Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs (Q3460055) (← 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)
- A Functional Framework for Result Checking (Q3558330) (← links)
- Certificate Translation for Optimizing Compilers (Q3613391) (← links)
- Formal Certification of ElGamal Encryption (Q3619468) (← links)
- (Q4218107) (← links)
