| Publication | Date of Publication | Type |
|---|
| A denotationally-based program logic for higher-order store | 2026-04-02 | Paper |
| Towards univalent reference types: the impact of univalence on denotational semantics | 2026-02-19 | Paper |
Controlling unfolding in type theory
Mathematical Structures in Computer Science | 2025-12-30 | Paper |
| Idempotent resources in separation logic. The heart of \texttt{core} in Iris | 2025-12-04 | Paper |
A logical approach to type soundness
Journal of the ACM | 2025-04-25 | Paper |
Cerise: program verification on a capability machine in the presence of untrusted code
Journal of the ACM | 2025-02-05 | Paper |
Unifying cubical and multimodal type theory
Logical Methods in Computer Science | 2025-01-31 | Paper |
| {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
Programming Languages and Systems | 2022-10-13 | Paper |
Modalities and Parametric Adjoints
ACM Transactions on Computational Logic | 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
Journal of Functional Programming | 2021-12-13 | Paper |
scientific article; zbMATH DE number 7407781 (Why is no real title available?)
(available as arXiv preprint) | 2021-10-08 | Paper |
| scientific article; zbMATH DE number 7407781 (Why is no real title available?) | 2021-10-08 | Paper |
Multimodal dependent type theory
(available as arXiv preprint) | 2021-10-08 | Paper |
| Multimodal dependent type theory | 2021-10-08 | Paper |
Multimodal dependent type theory
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-21 | Paper |
ReLoC: a mechanised relational logic for fine-grained concurrency
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
Modal dependent type theory and dependent right adjoints
Mathematical Structures in Computer Science | 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
(available as arXiv preprint) | 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
Journal of Automated Reasoning | 2019-08-21 | Paper |
Guarded cubical type theory
Journal of Automated Reasoning | 2019-08-21 | Paper |
Iris from the ground up: a modular foundation for higher-order concurrent separation logic
Journal of Functional Programming | 2019-02-20 | Paper |
A model of guarded recursion via generalised equilogical spaces
Theoretical Computer Science | 2018-03-12 | Paper |
Interactive proofs in higher-order concurrent separation logic
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | Paper |
A relational model of types-and-effects in higher-order concurrent separation logic
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | Paper |
Guarded cubical type theory: path equality for guarded recursion
(available as arXiv preprint) | 2017-07-19 | Paper |
Intensional type theory with guarded recursive types qua fixed points on universes
2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science | 2017-07-03 | Paper |
Caper
Programming Languages and Systems | 2017-05-19 | Paper |
The essence of higher-order concurrent separation logic
Programming Languages and Systems | 2017-05-19 | Paper |
Higher-order ghost state
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
Logical Methods in Computer Science | 2017-04-11 | Paper |
A model of PCF in guarded type theory
Electronic Notes in Theoretical Computer Science | 2016-12-16 | Paper |
Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-09-29 | Paper |
Step-indexed Kripke model of separation logic for storable locks
Electronic Notes in Theoretical Computer Science | 2016-07-15 | Paper |
A Kripke logical relation for effect-based program transformations
Information and Computation | 2016-07-07 | Paper |
Guarded dependent type theory with coinductive types
Lecture Notes in Computer Science | 2016-06-10 | Paper |
A separation logic for fictional sequential consistency
Programming Languages and Systems | 2016-04-26 | Paper |
Transfinite step-indexing: decoupling concrete and logical steps
Programming Languages and Systems | 2016-04-26 | Paper |
Local reasoning about a copying garbage collector
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-11-11 | Paper |
Step-indexed logical relations for probability
Lecture Notes in Computer Science | 2015-10-01 | Paper |
Programming and reasoning with guarded recursion for coinductive types
Lecture Notes in Computer Science | 2015-10-01 | Paper |
ModuRes: a Coq library for modular reasoning about concurrent higher-order imperative programming languages
Interactive Theorem Proving | 2015-09-14 | Paper |
Polymorphism and separation in Hoare type theory
Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming | 2015-08-03 | Paper |
A relational modal logic for higher-order stateful ADTs
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-06-11 | Paper |
Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
Proceedings of the 18th ACM SIGPLAN international conference on Functional programming | 2015-03-30 | Paper |
Ynot: dependent types for imperative programs
Proceedings of the 13th ACM SIGPLAN international conference on Functional programming | 2015-03-16 | Paper |
The impact of higher-order state and control effects on local relational reasoning
Proceedings of the 15th ACM SIGPLAN international conference on Functional programming | 2015-03-05 | Paper |
A Kripke logical relation for effect-based program transformations
Proceedings of the 16th ACM SIGPLAN international conference on Functional programming | 2015-03-05 | Paper |
Views, compositional reasoning for concurrent programs
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-11-27 | Paper |
Logical relations for fine-grained concurrency
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-11-27 | Paper |
A model of countable nondeterminism in guarded type theory
Lecture Notes in Computer Science | 2014-07-24 | Paper |
Higher-order separation logic in Isabelle/HOLCF
Electronic Notes in Theoretical Computer Science | 2014-05-13 | Paper |
Impredicative concurrent abstract predicates
Programming Languages and Systems | 2014-04-16 | Paper |
Modular reasoning about concurrent higher-order imperative programs
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Step-indexed Kripke models over recursive worlds
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-04-10 | Paper |
Matching of bigraphs
Electronic Notes in Theoretical Computer Science | 2013-12-20 | Paper |
Step-indexed relational reasoning for countable nondeterminism
Logical Methods in Computer Science | 2013-10-16 | Paper |
| Parametric domain-theoretic models of polymorphic intuitionistic/linear lambda calculus | 2013-10-08 | Paper |
| Synthetic domain theory and models of linear Abadi \& Plotkin logic | 2013-10-08 | Paper |
Modular reasoning about separation of concurrent data structures
Programming Languages and Systems | 2013-08-05 | Paper |
An inductive characterization of matching in binding bigraphs
Formal Aspects of Computing | 2013-03-22 | Paper |
A step-indexed Kripke model of hidden state
Mathematical Structures in Computer Science | 2013-03-14 | Paper |
| A concurrent logical relation | 2012-11-22 | Paper |
The impact of higher-order state and control effects on local relational reasoning
Journal of Functional Programming | 2012-10-29 | Paper |
First steps in synthetic guarded domain theory: step-indexing in the topos of trees
Logical Methods in Computer Science | 2012-10-22 | Paper |
Two for the price of one: lifting separation logic assertions
Logical Methods in Computer Science | 2012-09-25 | Paper |
Charge! A framework for higher-order separation logic in Coq
Interactive Theorem Proving | 2012-09-20 | Paper |
Step-indexed relational reasoning for countable nondeterminism
(available as arXiv preprint) | 2012-09-18 | Paper |
| Step-indexed relational reasoning for countable nondeterminism | 2012-09-18 | Paper |
A relational realizability model for higher-order stateful ADTs
The Journal of Logic and Algebraic Programming | 2012-08-14 | Paper |
Fictional separation logic
Programming Languages and Systems | 2012-06-22 | Paper |
Nested Hoare triples and frame rules for higher-order store
Logical Methods in Computer Science | 2012-04-02 | Paper |
Verifying object-oriented programs with higher-order separation logic in Coq
Interactive Theorem Proving | 2011-08-17 | Paper |
Partiality, state and dependent types
Lecture Notes in Computer Science | 2011-06-17 | Paper |
A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces
Foundations of Software Science and Computational Structures | 2011-05-19 | Paper |
The category-theoretic solution of recursive metric-space equations
Theoretical Computer Science | 2010-11-11 | Paper |
Realisability semantics of parametric polymorphism, general references and recursive types
Mathematical Structures in Computer Science | 2010-08-26 | Paper |
A semantic foundation for hidden state
Foundations of Software Science and Computational Structures | 2010-04-27 | Paper |
Nested Hoare Triples and Frame Rules for Higher-Order Store
Computer Science Logic | 2009-11-12 | Paper |
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
Foundations of Software Science and Computational Structures | 2009-03-31 | Paper |
Hoare type theory, polymorphism and separation
Journal of Functional Programming | 2008-12-18 | Paper |
On the Construction of Sorted Reactive Systems
CONCUR 2008 - Concurrency Theory | 2008-11-25 | Paper |
Synthetic domain theory and models of linear Abadi {\&} Plotkin logic
Annals of Pure and Applied Logic | 2008-11-12 | Paper |
A Simple Model of Separation Logic for Higher-Order Store
Automata, Languages and Programming | 2008-08-19 | Paper |
Relational Parametricity and Separation Logic
Logical Methods in Computer Science | 2008-08-07 | Paper |
Relational Reasoning for Recursive Types and References
Programming Languages and Systems | 2008-05-06 | Paper |
| Category-theoretic models of linear Abadi \& Plotkin logic | 2008-04-15 | Paper |
| Category-theoretic models of linear Abadi \& Plotkin logic | 2008-04-15 | Paper |
A Realizability Model for Impredicative Hoare Type Theory
Programming Languages and Systems | 2008-04-11 | Paper |
Domain-theoretical models of parametric polymorphism
Theoretical Computer Science | 2007-12-18 | Paper |
Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
Logical Methods in Computer Science | 2007-10-11 | Paper |
Linear Abadi and Plotkin Logic
Logical Methods in Computer Science | 2007-10-11 | Paper |
Relational Parametricity and Separation Logic
Foundations of Software Science and Computational Structures | 2007-09-07 | Paper |
Abstract Predicates and Mutable ADTs in Hoare Type Theory
Programming Languages and Systems | 2007-09-04 | Paper |
Sortings for Reactive Systems
CONCUR 2006 – Concurrency Theory | 2007-09-04 | Paper |
Foundations of Software Science and Computation Structures
Lecture Notes in Computer Science | 2007-05-02 | Paper |
| Axiomatizing binding bigraphs | 2007-04-10 | Paper |
Categorical models for Abadi and Plotkin's logic for parametricity
Mathematical Structures in Computer Science | 2005-10-18 | Paper |
Programming Languages and Systems
Lecture Notes in Computer Science | 2005-09-13 | Paper |
A retrospective on region-based memory management
Higher-Order and Symbolic Computation | 2005-03-15 | Paper |
Equilogical spaces
Theoretical Computer Science | 2004-08-06 | Paper |
