| Publication | Date of Publication | Type |
|---|
| {mitten}: a flexible multimodal proof assistant | 2024-11-26 | Paper |
| A stratified approach to Löb induction | 2024-05-27 | Paper |
| Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems | 2022-10-13 | Paper |
| Modalities and Parametric Adjoints | 2022-04-29 | Paper |
| On models of higher-order separation logic | 2022-04-25 | Paper |
| StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities | 2021-12-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5155670 | 2021-10-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5155672 | 2021-10-08 | Paper |
| Multimodal Dependent Type Theory | 2021-01-21 | Paper |
| ReLoC | 2021-01-20 | Paper |
| Modal dependent type theory and dependent right adjoints | 2020-03-11 | Paper |
| Compositional non-interference for concurrent programs via separation and framing | 2019-09-16 | Paper |
| Relational reasoning for Markov chains in a probabilistic guarded lambda calculus | 2019-09-13 | Paper |
| Reasoning about a machine with local capabilities. Provably safe stack and return pointer management | 2019-09-13 | Paper |
| Guarded cubical type theory | 2019-08-21 | Paper |
| Iris from the ground up: A modular foundation for higher-order concurrent separation logic | 2019-02-20 | Paper |
| A model of guarded recursion via generalised equilogical spaces | 2018-03-12 | Paper |
| Interactive proofs in higher-order concurrent separation logic | 2017-10-20 | Paper |
| A relational model of types-and-effects in higher-order concurrent separation logic | 2017-10-20 | Paper |
| Guarded Cubical Type Theory: Path Equality for Guarded Recursion | 2017-07-19 | Paper |
| Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes | 2017-07-03 | Paper |
| Caper | 2017-05-19 | Paper |
| The Essence of Higher-Order Concurrent Separation Logic | 2017-05-19 | Paper |
| Higher-order ghost state | 2017-05-10 | Paper |
| The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types | 2017-04-11 | Paper |
| A model of PCF in guarded type theory | 2016-12-16 | Paper |
| Iris | 2016-09-29 | Paper |
| Step-Indexed Kripke Model of Separation Logic for Storable Locks | 2016-07-15 | Paper |
| A Kripke logical relation for effect-based program transformations | 2016-07-07 | Paper |
| Guarded Dependent Type Theory with Coinductive Types | 2016-06-10 | Paper |
| A Separation Logic for Fictional Sequential Consistency | 2016-04-26 | Paper |
| Transfinite Step-Indexing: Decoupling Concrete and Logical Steps | 2016-04-26 | Paper |
| Local reasoning about a copying garbage collector | 2015-11-11 | Paper |
| Step-Indexed Logical Relations for Probability | 2015-10-01 | Paper |
| Programming and Reasoning with Guarded Recursion for Coinductive Types | 2015-10-01 | Paper |
| ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages | 2015-09-14 | Paper |
| Polymorphism and separation in hoare type theory | 2015-08-03 | Paper |
| A relational modal logic for higher-order stateful ADTs | 2015-06-11 | Paper |
| Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency | 2015-03-30 | Paper |
| Ynot | 2015-03-16 | Paper |
| The impact of higher-order state and control effects on local relational reasoning | 2015-03-05 | Paper |
| A kripke logical relation for effect-based program transformations | 2015-03-05 | Paper |
| Views | 2014-11-27 | Paper |
| Logical relations for fine-grained concurrency | 2014-11-27 | Paper |
| A Model of Countable Nondeterminism in Guarded Type Theory | 2014-07-24 | Paper |
| Higher-Order Separation Logic in Isabelle/HOLCF | 2014-05-13 | Paper |
| Impredicative Concurrent Abstract Predicates | 2014-04-16 | Paper |
| Modular reasoning about concurrent higher-order imperative programs | 2014-04-10 | Paper |
| Step-indexed kripke models over recursive worlds | 2014-04-10 | Paper |
| Matching of Bigraphs | 2013-12-20 | Paper |
| Step-Indexed Relational Reasoning for Countable Nondeterminism | 2013-10-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2852350 | 2013-10-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2852351 | 2013-10-08 | Paper |
| Modular Reasoning about Separation of Concurrent Data Structures | 2013-08-05 | Paper |
| An inductive characterization of matching in binding bigraphs | 2013-03-22 | Paper |
| A step-indexed Kripke model of hidden state | 2013-03-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4649541 | 2012-11-22 | Paper |
| The impact of higher-order state and control effects on local relational reasoning | 2012-10-29 | Paper |
| First steps in synthetic guarded domain theory: step-indexing in the topos of trees | 2012-10-22 | Paper |
| Two for the Price of One: Lifting Separation Logic Assertions | 2012-09-25 | Paper |
| Charge! | 2012-09-20 | Paper |
| Step-Indexed Relational Reasoning for Countable Nondeterminism | 2012-09-18 | Paper |
| A relational realizability model for higher-order stateful ADTs | 2012-08-14 | Paper |
| Fictional Separation Logic | 2012-06-22 | Paper |
| Nested Hoare Triples and Frame Rules for Higher-order Store | 2012-04-02 | Paper |
| Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq | 2011-08-17 | Paper |
| Partiality, State and Dependent Types | 2011-06-17 | Paper |
| A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces | 2011-05-19 | Paper |
| The category-theoretic solution of recursive metric-space equations | 2010-11-11 | Paper |
| Realisability semantics of parametric polymorphism, general references and recursive types | 2010-08-26 | Paper |
| A Semantic Foundation for Hidden State | 2010-04-27 | Paper |
| Nested Hoare Triples and Frame Rules for Higher-Order Store | 2009-11-12 | Paper |
| Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types | 2009-03-31 | Paper |
| Hoare type theory, polymorphism and separation | 2008-12-18 | Paper |
| On the Construction of Sorted Reactive Systems | 2008-11-25 | Paper |
| Synthetic domain theory and models of linear Abadi {\&} Plotkin logic | 2008-11-12 | Paper |
| A Simple Model of Separation Logic for Higher-Order Store | 2008-08-19 | Paper |
| Relational Parametricity and Separation Logic | 2008-08-07 | Paper |
| Relational Reasoning for Recursive Types and References | 2008-05-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5458501 | 2008-04-15 | Paper |
| A Realizability Model for Impredicative Hoare Type Theory | 2008-04-11 | Paper |
| Domain-theoretical models of parametric polymorphism | 2007-12-18 | Paper |
| Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages | 2007-10-11 | Paper |
| Linear Abadi and Plotkin Logic | 2007-10-11 | Paper |
| Relational Parametricity and Separation Logic | 2007-09-07 | Paper |
| Abstract Predicates and Mutable ADTs in Hoare Type Theory | 2007-09-04 | Paper |
| Sortings for Reactive Systems | 2007-09-04 | Paper |
| Foundations of Software Science and Computation Structures | 2007-05-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3431406 | 2007-04-10 | Paper |
| Categorical models for Abadi and Plotkin's logic for parametricity | 2005-10-18 | Paper |
| Programming Languages and Systems | 2005-09-13 | Paper |
| A retrospective on region-based memory management | 2005-03-15 | Paper |
| Equilogical spaces | 2004-08-06 | Paper |
| A General Notion of Realizability | 2004-03-01 | Paper |
| Elementary axioms for local maps of toposes | 2003-03-09 | Paper |
| Relational interpretations of recursive types in an operational setting. | 2003-01-14 | Paper |
| Relative and modified relative realizability | 2002-12-02 | Paper |
| Local realizability toposes and a modal logic for computability | 2002-10-31 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2753674 | 2001-12-03 | Paper |
| A constraint-based region inference algorithm | 2001-08-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4499148 | 2001-03-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4499150 | 2001-03-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4513576 | 2001-02-28 | Paper |
| Developing theories of types and computability via realizability | 2000-08-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4364397 | 1997-11-17 | Paper |
