| Publication | Date of Publication | Type |
|---|
| Automata theory and logic. Translated from the German by the authors. Revised and extended English edition | 2025-11-26 | Paper |
A quantitative model for simply typed λ-calculus
Mathematical Structures in Computer Science | 2023-02-06 | Paper |
Type-based analysis of logarithmic amortised complexity
Mathematical Structures in Computer Science | 2023-02-06 | Paper |
Categorical reconstruction of a reduction free normalization proof
Category Theory and Computer Science | 2022-12-16 | Paper |
On behavioural abstraction and behavioural satisfaction in higher-order logic
TAPSOFT '95: Theory and Practice of Software Development | 2022-08-18 | Paper |
| Learn with SAT to minimize Büchi automata | 2021-04-27 | Paper |
Learn with SAT to minimize Büchi automata
(available as arXiv preprint) | 2021-04-27 | Paper |
| scientific article; zbMATH DE number 7297868 (Why is no real title available?) | 2021-01-19 | Paper |
Decidable inequalities over infinite trees
EPiC Series in Computing | 2019-07-04 | Paper |
| Extensional Constructs in Intensional Type Theory | 2019-04-26 | Paper |
| Modular edit lenses | 2019-02-15 | Paper |
Conservativity of equality reflection over intensional type theory
Lecture Notes in Computer Science | 2019-01-15 | Paper |
Decidable linear list constraints
EPiC Series in Computing | 2019-01-10 | Paper |
Proof-relevant logical relations for name generation
Logical Methods in Computer Science | 2018-04-25 | Paper |
Abstract interpretation from Büchi automata
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) | 2018-04-23 | Paper |
| Multivariate amortised resource analysis for term rewrite systems | 2017-07-12 | Paper |
| Computing with a fixed number of pointers (invited talk) | 2017-02-21 | Paper |
Counting successes: effects and transformations for non-deterministic programs
A List of Successes That Can Change the World | 2016-08-17 | Paper |
Certification for \(\mu \)-calculus with winning strategies
Model Checking Software | 2016-06-22 | Paper |
Pure pointer programs with iteration
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Edit lenses
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
Static prediction of heap space usage for first-order functional programs
Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
Logical relations and nondeterminism
Software, Services, and Systems | 2015-06-22 | Paper |
Static determination of quantitative resource usage for higher-order programs
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-06-11 | Paper |
The strength of non-size increasing computation
Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-03-17 | Paper |
Revisiting the categorical interpretation of dependent type theory
Theoretical Computer Science | 2014-07-25 | Paper |
Amortised resource analysis and typed polynomial interpretations
Lecture Notes in Computer Science | 2014-07-24 | Paper |
Verifying pointer and string analyses with region type systems
Computer Languages, Systems & Structures | 2014-06-16 | Paper |
Multivariate amortized resource analysis
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-04-10 | Paper |
Symmetric lenses
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-04-10 | Paper |
Abstract effects and proof-relevant logical relations
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Automatic type inference for amortised heap-space analysis
Programming Languages and Systems | 2013-08-05 | Paper |
Proof-relevant logical relations for name generation
Lecture Notes in Computer Science | 2013-06-28 | Paper |
Pure Pointer Programs and Tree Isomorphism
Lecture Notes in Computer Science | 2013-03-18 | Paper |
On monadic parametricity of second-order functionals
Lecture Notes in Computer Science | 2013-03-18 | Paper |
Linear constraints over infinite trees
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
Realizability models and implicit complexity
Theoretical Computer Science | 2011-05-10 | Paper |
Automatentheorie und Logik
eXamen.press | 2011-03-22 | Paper |
Verifying pointer and string analyses with region type systems
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-01-07 | Paper |
Bounded linear logic, revisited
Logical Methods in Computer Science | 2010-12-20 | Paper |
Verifying a local generic solver in Coq
Static Analysis | 2010-10-01 | Paper |
What is a pure functional?
Automata, Languages and Programming | 2010-09-07 | Paper |
A semantic proof of polytime soundness of light affine logic
Theory of Computing Systems | 2010-08-13 | Paper |
Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs
Programming Languages and Systems | 2010-05-04 | Paper |
Efficient Type-Checking for Amortised Heap-Space Analysis
Computer Science Logic | 2009-11-12 | Paper |
Bounded Linear Logic, Revisited
Lecture Notes in Computer Science | 2009-07-07 | Paper |
Certification Using the Mobius Base Logic
Formal Methods for Components and Objects | 2009-02-12 | Paper |
Nominal Renaming Sets
Logic for Programming, Artificial Intelligence, and Reasoning | 2009-01-27 | Paper |
Pure Pointer Programs with Iteration
Computer Science Logic | 2008-11-20 | Paper |
A Semantic Proof of Polytime Soundness of Light Affine Logic
Computer Science – Theory and Applications | 2008-06-05 | Paper |
Reading, Writing and Relations
Programming Languages and Systems | 2008-05-06 | Paper |
A Bytecode Logic for JML and Types
Programming Languages and Systems | 2008-05-06 | Paper |
A Proof System for the Linear Time μ-Calculus
FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science | 2008-04-17 | Paper |
A type system with usage aspects
Journal of Functional Programming | 2008-03-27 | Paper |
Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories
Pillars of Computer Science | 2008-03-25 | Paper |
A program logic for resources
Theoretical Computer Science | 2007-12-14 | Paper |
Programming Languages and Systems
Lecture Notes in Computer Science | 2007-05-02 | Paper |
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
Lecture Notes in Computer Science | 2006-11-14 | Paper |
Well-foundedness in realizability
Archive for Mathematical Logic | 2006-11-06 | Paper |
Completeness of continuation models for \(\lambda_\mu\)-calculus
Information and Computation | 2006-10-10 | Paper |
Logic for Programming, Artificial Intelligence, and Reasoning
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Automata, Languages and Programming
Lecture Notes in Computer Science | 2005-08-24 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2005-08-18 | Paper |
| scientific article; zbMATH DE number 2185663 (Why is no real title available?) | 2005-07-04 | Paper |
On the non-sequential nature of the interval-domain model of real-number computation
Mathematical Structures in Computer Science | 2005-03-21 | Paper |
| scientific article; zbMATH DE number 2087536 (Why is no real title available?) | 2004-08-11 | Paper |
Realizability models for BLL-like languages
Theoretical Computer Science | 2004-08-06 | Paper |
An arithmetic for non-size-increasing polynomial-time computation
Theoretical Computer Science | 2004-08-06 | Paper |
| scientific article; zbMATH DE number 2079044 (Why is no real title available?) | 2004-07-21 | Paper |
Linear types and non-size-increasing polynomial time computation.
Information and Computation | 2003-08-19 | Paper |
Type destructors
Information and Computation | 2003-01-14 | Paper |
| scientific article; zbMATH DE number 1834639 (Why is no real title available?) | 2002-11-25 | Paper |
A new “feasible” arithmetic
Journal of Symbolic Logic | 2002-10-29 | Paper |
| scientific article; zbMATH DE number 1670748 (Why is no real title available?) | 2001-12-18 | Paper |
A type system for bounded space and functional in-place update
Nordic Journal of Computing | 2001-11-07 | Paper |
Semantics of linear/modal lambda calculus
Journal of Functional Programming | 2001-07-15 | Paper |
| scientific article; zbMATH DE number 1538025 (Why is no real title available?) | 2001-02-05 | Paper |
Safe recursion with higher types and BCK-algebra
Annals of Pure and Applied Logic | 2000-09-04 | Paper |
An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras
The Bulletin of Symbolic Logic | 2000-02-28 | Paper |
An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras
The Bulletin of Symbolic Logic | 2000-02-28 | Paper |
| scientific article; zbMATH DE number 1302059 (Why is no real title available?) | 2000-02-15 | Paper |
A new method for establishing conservativity of classical systems over their intuitionistic version
Mathematical Structures in Computer Science | 1999-11-25 | Paper |
| scientific article; zbMATH DE number 1241699 (Why is no real title available?) | 1999-01-18 | Paper |
| scientific article; zbMATH DE number 1223626 (Why is no real title available?) | 1998-11-15 | Paper |
On behavioural abstraction and behavioural satisfaction in higher-order logic
Theoretical Computer Science | 1997-02-27 | Paper |
Sound and complete axiomatisations of call-by-value control operators
Mathematical Structures in Computer Science | 1996-07-15 | Paper |
Positive subtyping
Information and Computation | 1996-07-03 | Paper |
