| Publication | Date of Publication | Type |
|---|
| Approximate span liftings. Compositional semantics for relaxations of differential privacy | 2024-12-19 | Paper |
| Quantum weakest preconditions for reasoning about expected runtimes of quantum programs | 2024-12-06 | Paper |
| Formally verifying Kyber. Episode V: machine-checked IND-CCA security and correctness of ML-KEM in Easycrypt | 2024-12-04 | Paper |
| Congruence types | 2024-06-21 | Paper |
Fixing and mechanizing the security proof of Fiat-Shamir with aborts and Dilithium
Advances in Cryptology – CRYPTO 2023 | 2024-02-06 | Paper |
Masking the GLP lattice-based signature scheme at any order
Journal of Cryptology | 2024-01-23 | Paper |
Semantic foundations for cost analysis of pipeline-optimized programs
Static Analysis | 2023-07-28 | Paper |
A simple abstract semantics for equational theories
Fundamentals of Computation Theory | 2022-12-09 | Paper |
Universal Equivalence and Majority of Probabilistic Programs over Finite Fields
ACM Transactions on Computational Logic | 2022-12-08 | Paper |
On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem
Programming Languages and Systems | 2022-10-13 | Paper |
A formal treatment of the role of verified compilers in secure computation
Journal of Logical and Algebraic Methods in Programming | 2022-03-09 | Paper |
scientific article; zbMATH DE number 7376040 (Why is no real title available?)
(available as arXiv preprint) | 2021-07-28 | Paper |
System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
Journal of Automated Reasoning | 2021-02-17 | Paper |
Probabilistic Couplings from Program Logics
Foundations of Probabilistic Programming | 2021-02-16 | Paper |
Universal equivalence and majority of probabilistic programs over finite fields
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-21 | 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
(available as arXiv preprint) | 2020-01-03 | Paper |
Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
Journal of Automated Reasoning | 2019-10-25 | Paper |
An assertion-based program logic for probabilistic programs
(available as arXiv preprint) | 2019-09-13 | Paper |
Relational reasoning for Markov chains in a probabilistic guarded lambda calculus
(available as arXiv preprint) | 2019-09-13 | Paper |
Automated analysis of cryptographic assumptions in generic group models
Journal of Cryptology | 2019-06-20 | Paper |
System-level non-interference of constant-time cryptography. I: Model
Journal of Automated Reasoning | 2019-05-31 | Paper |
| Privacy Amplification by Mixing and Diffusion Mechanisms | 2019-05-29 | Paper |
Synthesizing Probabilistic Invariants via Doob’s Decomposition
Computer Aided Verification | 2019-05-03 | Paper |
A two-level approach towards lean proof-checking
Lecture Notes in Computer Science | 2019-01-15 | Paper |
Implicit coercions in type systems
Lecture Notes in Computer Science | 2019-01-15 | Paper |
Modular properties of algebraic type systems
Higher-Order Algebra, Logic, and Term Rewriting | 2019-01-11 | Paper |
Proving uniformity and independence by self-composition and coupling
EPiC Series in Computing | 2019-01-10 | Paper |
| Masking the GLP lattice-based signature scheme at any order | 2018-07-09 | Paper |
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC
Fast Software Encryption | 2018-05-09 | 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?)
(available as arXiv preprint) | 2017-12-19 | Paper |
| Generic transformations of predicate encodings: constructions and applications | 2017-11-03 | Paper |
Relational cost analysis
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | 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 |
Is Your Software on Dope?
Programming Languages and Systems | 2017-05-19 | Paper |
| Formally verified implementation of an idealized model of virtualization | 2017-03-13 | Paper |
Computer-aided verification for mechanism design
Web and Internet Economics | 2017-02-10 | Paper |
Product programs and relational program logics
Journal of Logical and Algebraic Methods in Programming | 2016-12-15 | 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 |
Automated unbounded analysis of cryptographic constructions in the generic group model
Advances in Cryptology – EUROCRYPT 2016 | 2016-07-15 | Paper |
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Relational reasoning via probabilistic coupling
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Beyond 2-safety: asymmetric product programs for relational program verification
Logical Foundations of Computer Science | 2015-12-11 | Paper |
Verified Proofs of Higher-Order Masking
Advances in Cryptology -- EUROCRYPT 2015 | 2015-09-30 | Paper |
Mind the gap: modular machine-checked proofs of one-round key exchange protocols
Advances in Cryptology - EUROCRYPT 2015 | 2015-09-30 | Paper |
Probabilistic relational reasoning for differential privacy
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
Pure patterns type systems
Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds
Lecture Notes in Computer Science | 2015-08-27 | Paper |
Making RSA–PSS Provably Secure against Non-random Faults
Advanced Information Systems Engineering | 2015-07-21 | Paper |
Formal certification of code-based cryptographic proofs
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-07-03 | Paper |
EasyCrypt: a tutorial
Foundations of Security Analysis and Design VII | 2015-05-27 | Paper |
Automated analysis of cryptographic assumptions in generic group models
Advances in Cryptology – CRYPTO 2014 | 2014-08-07 | Paper |
Probabilistic relational verification for cryptographic implementations
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
A certified lightweight non-interference Java bytecode verifier
Mathematical Structures in Computer Science | 2014-03-12 | Paper |
Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs
Automata, Languages, and Programming | 2013-08-07 | Paper |
Computer-aided cryptographic proofs
Interactive Theorem Proving | 2012-09-20 | Paper |
Probabilistic relational Hoare logics for computer-aided security proofs
Lecture Notes in Computer Science | 2012-09-05 | Paper |
Verified indifferentiable hashing into elliptic curves
Lecture Notes in Computer Science | 2012-06-29 | Paper |
A computational indistinguishability logic for the bounded storage model
Foundations and Practice of Security | 2012-06-08 | Paper |
Secure information flow by self-composition
Mathematical Structures in Computer Science | 2011-12-08 | Paper |
Verifiable security of Boneh-Franklin identity-based encryption
Provable Security | 2011-09-16 | Paper |
Computer-Aided Security Proofs for the Working Cryptographer
Advances in Cryptology – CRYPTO 2011 | 2011-08-12 | Paper |
Beyond provable security verifiable IND-CCA security of OAEP
Topics in Cryptology – CT-RSA 2011 | 2011-02-11 | Paper |
On the equality of probabilistic terms
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-01-07 | Paper |
Programming language techniques for cryptographic proofs
Interactive Theorem Proving | 2010-09-14 | Paper |
A functional framework for result checking
Functional and Logic Programming | 2010-05-04 | Paper |
An Introduction to Certificate Translation
Foundations of Security Analysis and Design V | 2009-10-22 | Paper |
A Tutorial on Type-Based Termination
Language Engineering and Rigorous Software Development | 2009-07-28 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2009-05-15 | Paper |
Formal Certification of ElGamal Encryption
Formal Aspects in Security and Trust | 2009-04-07 | Paper |
Certificate Translation for Optimizing Compilers
Static Analysis | 2009-03-12 | Paper |
Preservation of Proof Obligations from Java to the Java Virtual Machine
Automated Reasoning | 2008-11-27 | Paper |
Type-Based Termination with Sized Products
Computer Science Logic | 2008-11-20 | Paper |
CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Certificate Translation in Abstract Interpretation
Programming Languages and Systems | 2008-04-11 | Paper |
Fundamental Approaches to Software Engineering
Lecture Notes in Computer Science | 2007-11-28 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
A Certified Lightweight Non-interference Java Bytecode Verifier
Programming Languages and Systems | 2007-09-04 | Paper |
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
Functional and Logic Programming | 2007-05-02 | Paper |
Security types preserving compilation
Computer Languages, Systems & Structures | 2007-02-20 | Paper |
Tool-assisted specification and verification of typed low-level languages
Journal of Automated Reasoning | 2007-01-30 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2006-11-13 | Paper |
Remarks on the equational theory of non-normalizing pure type systems
Journal of Functional Programming | 2006-03-22 | Paper |
A computational view of implicit coercions in type theory
Mathematical Structures in Computer Science | 2006-03-10 | Paper |
Typed Lambda Calculi and Applications
Lecture Notes in Computer Science | 2005-11-11 | Paper |
| scientific article; zbMATH DE number 2185650 (Why is no real title available?) | 2005-07-04 | Paper |
Remarks on the equational theory of non-normalizing pure type systems
Journal of Functional Programming | 2004-09-24 | Paper |
| scientific article; zbMATH DE number 2090721 (Why is no real title available?) | 2004-08-13 | Paper |
| scientific article; zbMATH DE number 2087509 (Why is no real title available?) | 2004-08-11 | Paper |
| scientific article; zbMATH DE number 2086505 (Why is no real title available?) | 2004-08-11 | Paper |
Setoids in type theory
Journal of Functional Programming | 2004-03-17 | Paper |
| scientific article; zbMATH DE number 2043539 (Why is no real title available?) | 2004-02-16 | Paper |
| scientific article; zbMATH DE number 1927413 (Why is no real title available?) | 2003-06-12 | Paper |
| scientific article; zbMATH DE number 1848374 (Why is no real title available?) | 2003-01-05 | Paper |
| scientific article; zbMATH DE number 1696586 (Why is no real title available?) | 2002-07-22 | Paper |
| scientific article; zbMATH DE number 1696775 (Why is no real title available?) | 2002-07-22 | Paper |
An induction principle for pure type systems
Theoretical Computer Science | 2002-03-03 | Paper |
Weak normalization implies strong normalization in a class of non-dependent pure type systems
Theoretical Computer Science | 2002-03-03 | Paper |
Domain-free pure type systems
Journal of Functional Programming | 2002-02-17 | Paper |
| scientific article; zbMATH DE number 1701346 (Why is no real title available?) | 2002-02-05 | Paper |
| scientific article; zbMATH DE number 1692947 (Why is no real title available?) | 2002-01-21 | Paper |
Type-checking injective pure type systems
Journal of Functional Programming | 2000-12-06 | Paper |
| scientific article; zbMATH DE number 1512607 (Why is no real title available?) | 2000-10-03 | Paper |
| scientific article; zbMATH DE number 1330132 (Why is no real title available?) | 2000-03-13 | Paper |
CPS translations and applications: The cube and beyond
Higher-Order and Symbolic Computation | 2000-01-30 | Paper |
Order-sorted inductive types
Information and Computation | 2000-01-09 | Paper |
| scientific article; zbMATH DE number 1342216 (Why is no real title available?) | 1999-09-22 | Paper |
| scientific article; zbMATH DE number 1223736 (Why is no real title available?) | 1999-02-14 | Paper |
| scientific article; zbMATH DE number 1231611 (Why is no real title available?) | 1999-01-06 | Paper |
| scientific article; zbMATH DE number 1231563 (Why is no real title available?) | 1998-12-20 | Paper |
| scientific article; zbMATH DE number 1222569 (Why is no real title available?) | 1998-11-11 | Paper |
| scientific article; zbMATH DE number 1114328 (Why is no real title available?) | 1998-05-17 | Paper |
| scientific article; zbMATH DE number 1088029 (Why is no real title available?) | 1998-04-01 | Paper |
| scientific article; zbMATH DE number 1086659 (Why is no real title available?) | 1997-11-13 | Paper |
