| 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 | 2024-02-06 | Paper |
| Masking the GLP lattice-based signature scheme at any order | 2024-01-23 | Paper |
| Semantic foundations for cost analysis of pipeline-optimized programs | 2023-07-28 | Paper |
| A simple abstract semantics for equational theories | 2022-12-09 | Paper |
| Universal Equivalence and Majority of Probabilistic Programs over Finite Fields | 2022-12-08 | Paper |
| On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem | 2022-10-13 | Paper |
| A formal treatment of the role of verified compilers in secure computation | 2022-03-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5002798 | 2021-07-28 | Paper |
| System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory | 2021-02-17 | Paper |
| Probabilistic Couplings from Program Logics | 2021-02-16 | Paper |
| Universal equivalence and majority of probabilistic programs over finite fields | 2021-01-21 | Paper |
| \(*\)-liftings for differential privacy | 2020-05-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5219933 | 2020-03-09 | Paper |
| Relational \(\star\)-liftings for differential privacy | 2020-01-03 | Paper |
| Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs | 2019-10-25 | Paper |
| An assertion-based program logic for probabilistic programs | 2019-09-13 | Paper |
| Relational reasoning for Markov chains in a probabilistic guarded lambda calculus | 2019-09-13 | Paper |
| Automated analysis of cryptographic assumptions in generic group models | 2019-06-20 | Paper |
| System-level non-interference of constant-time cryptography. I: Model | 2019-05-31 | Paper |
| Privacy Amplification by Mixing and Diffusion Mechanisms | 2019-05-29 | Paper |
| Synthesizing Probabilistic Invariants via Doob’s Decomposition | 2019-05-03 | Paper |
| A two-level approach towards lean proof-checking | 2019-01-15 | Paper |
| Implicit coercions in type systems | 2019-01-15 | Paper |
| Modular properties of algebraic type systems | 2019-01-11 | Paper |
| Proving uniformity and independence by self-composition and coupling | 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 | 2018-05-09 | Paper |
| Proving differential privacy via probabilistic couplings | 2018-04-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4598248 | 2017-12-19 | Paper |
| Generic transformations of predicate encodings: constructions and applications | 2017-11-03 | Paper |
| Relational cost analysis | 2017-10-20 | Paper |
| Coupling proofs are probabilistic product programs | 2017-10-20 | Paper |
| Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model | 2017-06-13 | Paper |
| Is Your Software on Dope? | 2017-05-19 | Paper |
| Formally verified implementation of an idealized model of virtualization | 2017-03-13 | Paper |
| Computer-aided verification for mechanism design | 2017-02-10 | Paper |
| Product programs and relational program logics | 2016-12-15 | Paper |
| Higher-order approximate relational refinement types for mechanism design and differential privacy | 2016-09-29 | Paper |
| Automated unbounded analysis of cryptographic constructions in the generic group model | 2016-07-15 | Paper |
| Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs | 2016-01-12 | Paper |
| Relational reasoning via probabilistic coupling | 2016-01-12 | Paper |
| Beyond 2-safety: asymmetric product programs for relational program verification | 2015-12-11 | Paper |
| Verified Proofs of Higher-Order Masking | 2015-09-30 | Paper |
| Mind the gap: modular machine-checked proofs of one-round key exchange protocols | 2015-09-30 | Paper |
| Probabilistic relational reasoning for differential privacy | 2015-09-11 | Paper |
| Pure patterns type systems | 2015-09-11 | Paper |
| Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds | 2015-08-27 | Paper |
| Making RSA–PSS Provably Secure against Non-random Faults | 2015-07-21 | Paper |
| Formal certification of code-based cryptographic proofs | 2015-07-03 | Paper |
| EasyCrypt: a tutorial | 2015-05-27 | Paper |
| Automated analysis of cryptographic assumptions in generic group models | 2014-08-07 | Paper |
| Probabilistic relational verification for cryptographic implementations | 2014-04-10 | Paper |
| A certified lightweight non-interference Java bytecode verifier | 2014-03-12 | Paper |
| Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs | 2013-08-07 | Paper |
| Computer-aided cryptographic proofs | 2012-09-20 | Paper |
| Probabilistic relational Hoare logics for computer-aided security proofs | 2012-09-05 | Paper |
| Verified indifferentiable hashing into elliptic curves | 2012-06-29 | Paper |
| A computational indistinguishability logic for the bounded storage model | 2012-06-08 | Paper |
| Secure information flow by self-composition | 2011-12-08 | Paper |
| Verifiable security of Boneh-Franklin identity-based encryption | 2011-09-16 | Paper |
| Computer-Aided Security Proofs for the Working Cryptographer | 2011-08-12 | Paper |
| Beyond provable security verifiable IND-CCA security of OAEP | 2011-02-11 | Paper |
| On the equality of probabilistic terms | 2011-01-07 | Paper |
| Programming language techniques for cryptographic proofs | 2010-09-14 | Paper |
| A functional framework for result checking | 2010-05-04 | Paper |
| An Introduction to Certificate Translation | 2009-10-22 | Paper |
| A Tutorial on Type-Based Termination | 2009-07-28 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2009-05-15 | Paper |
| Formal Certification of ElGamal Encryption | 2009-04-07 | Paper |
| Certificate Translation for Optimizing Compilers | 2009-03-12 | Paper |
| Preservation of Proof Obligations from Java to the Java Virtual Machine | 2008-11-27 | Paper |
| Type-Based Termination with Sized Products | 2008-11-20 | Paper |
| CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions | 2008-05-27 | Paper |
| Certificate Translation in Abstract Interpretation | 2008-04-11 | Paper |
| Fundamental Approaches to Software Engineering | 2007-11-28 | Paper |
| Automated Reasoning | 2007-09-25 | Paper |
| A Certified Lightweight Non-interference Java Bytecode Verifier | 2007-09-04 | Paper |
| Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant | 2007-05-02 | Paper |
| Security types preserving compilation | 2007-02-20 | Paper |
| Tool-assisted specification and verification of typed low-level languages | 2007-01-30 | Paper |
| Types for Proofs and Programs | 2006-11-13 | Paper |
| Remarks on the equational theory of non-normalizing pure type systems | 2006-03-22 | Paper |
| A computational view of implicit coercions in type theory | 2006-03-10 | Paper |
| Typed Lambda Calculi and Applications | 2005-11-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3024819 | 2005-07-04 | Paper |
| Remarks on the equational theory of non-normalizing pure type systems | 2004-09-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4813221 | 2004-08-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4738309 | 2004-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4736986 | 2004-08-11 | Paper |
| Setoids in type theory | 2004-03-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4447243 | 2004-02-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4484330 | 2003-06-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4785541 | 2003-01-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2766771 | 2002-07-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2767030 | 2002-07-22 | Paper |
| An induction principle for pure type systems | 2002-03-03 | Paper |
| Weak normalization implies strong normalization in a class of non-dependent pure type systems | 2002-03-03 | Paper |
| Domain-free pure type systems | 2002-02-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2769425 | 2002-02-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2763680 | 2002-01-21 | Paper |
| Type-checking injective pure type systems | 2000-12-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4508290 | 2000-10-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4260702 | 2000-03-13 | Paper |
| CPS translations and applications: The cube and beyond | 2000-01-30 | Paper |
| Order-sorted inductive types | 2000-01-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4263801 | 1999-09-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4219052 | 1999-02-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4222932 | 1999-01-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4222881 | 1998-12-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4218107 | 1998-11-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4376043 | 1998-05-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4364376 | 1998-04-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4362909 | 1997-11-13 | Paper |
