| Publication | Date of Publication | Type |
|---|
| A quantitative model for simply typed λ-calculus | 2023-02-06 | Paper |
| Type-based analysis of logarithmic amortised complexity | 2023-02-06 | Paper |
| Categorical reconstruction of a reduction free normalization proof | 2022-12-16 | Paper |
| On behavioural abstraction and behavioural satisfaction in higher-order logic | 2022-08-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4986506 | 2021-04-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5144667 | 2021-01-19 | Paper |
| Decidable Inequalities over Infinite Trees | 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 | 2019-01-15 | Paper |
| Decidable linear list constraints | 2019-01-10 | Paper |
| Proof-Relevant Logical Relations for Name Generation | 2018-04-25 | Paper |
| Abstract interpretation from Büchi automata | 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 | 2016-08-17 | Paper |
| Certification for $$\mu $$ μ -Calculus with Winning Strategies | 2016-06-22 | Paper |
| Pure pointer programs with iteration | 2015-09-17 | Paper |
| Edit lenses | 2015-09-11 | Paper |
| Static prediction of heap space usage for first-order functional programs | 2015-09-11 | Paper |
| Logical Relations and Nondeterminism | 2015-06-22 | Paper |
| Static determination of quantitative resource usage for higher-order programs | 2015-06-11 | Paper |
| The strength of non-size increasing computation | 2015-03-17 | Paper |
| Revisiting the categorical interpretation of dependent type theory | 2014-07-25 | Paper |
| Amortised Resource Analysis and Typed Polynomial Interpretations | 2014-07-24 | Paper |
| Verifying pointer and string analyses with region type systems | 2014-06-16 | Paper |
| Multivariate amortized resource analysis | 2014-04-10 | Paper |
| Symmetric lenses | 2014-04-10 | Paper |
| Abstract effects and proof-relevant logical relations | 2014-04-10 | Paper |
| Automatic Type Inference for Amortised Heap-Space Analysis | 2013-08-05 | Paper |
| Proof-Relevant Logical Relations for Name Generation | 2013-06-28 | Paper |
| Pure Pointer Programs and Tree Isomorphism | 2013-03-18 | Paper |
| On Monadic Parametricity of Second-Order Functionals | 2013-03-18 | Paper |
| Linear Constraints over Infinite Trees | 2012-06-15 | Paper |
| Realizability models and implicit complexity | 2011-05-10 | Paper |
| Automatentheorie und Logik | 2011-03-22 | Paper |
| Verifying Pointer and String Analyses with Region Type Systems | 2011-01-07 | Paper |
| Bounded Linear Logic, Revisited | 2010-12-20 | Paper |
| Verifying a Local Generic Solver in Coq | 2010-10-01 | Paper |
| What Is a Pure Functional? | 2010-09-07 | Paper |
| A semantic proof of polytime soundness of light affine logic | 2010-08-13 | Paper |
| Amortized Resource Analysis with Polynomial Potential | 2010-05-04 | Paper |
| Efficient Type-Checking for Amortised Heap-Space Analysis | 2009-11-12 | Paper |
| Bounded Linear Logic, Revisited | 2009-07-07 | Paper |
| Certification Using the Mobius Base Logic | 2009-02-12 | Paper |
| Nominal Renaming Sets | 2009-01-27 | Paper |
| Pure Pointer Programs with Iteration | 2008-11-20 | Paper |
| A Semantic Proof of Polytime Soundness of Light Affine Logic | 2008-06-05 | Paper |
| Reading, Writing and Relations | 2008-05-06 | Paper |
| A Bytecode Logic for JML and Types | 2008-05-06 | Paper |
| A Proof System for the Linear Time μ-Calculus | 2008-04-17 | Paper |
| A type system with usage aspects | 2008-03-27 | Paper |
| Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories | 2008-03-25 | Paper |
| A program logic for resources | 2007-12-14 | Paper |
| Programming Languages and Systems | 2007-05-02 | Paper |
| FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science | 2006-11-14 | Paper |
| Well-foundedness in realizability | 2006-11-06 | Paper |
| Completeness of continuation models for \(\lambda_\mu\)-calculus | 2006-10-10 | Paper |
| Logic for Programming, Artificial Intelligence, and Reasoning | 2005-11-10 | Paper |
| Automata, Languages and Programming | 2005-08-24 | Paper |
| Theorem Proving in Higher Order Logics | 2005-08-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3024837 | 2005-07-04 | Paper |
| On the non-sequential nature of the interval-domain model of real-number computation | 2005-03-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4738344 | 2004-08-11 | Paper |
| Realizability models for BLL-like languages | 2004-08-06 | Paper |
| An arithmetic for non-size-increasing polynomial-time computation | 2004-08-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4474857 | 2004-07-21 | Paper |
| Linear types and non-size-increasing polynomial time computation. | 2003-08-19 | Paper |
| Type destructors | 2003-01-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4779134 | 2002-11-25 | Paper |
| A new “feasible” arithmetic | 2002-10-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2754049 | 2001-12-18 | Paper |
| A type system for bounded space and functional in-place update | 2001-11-07 | Paper |
| Semantics of linear/modal lambda calculus | 2001-07-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4518880 | 2001-02-05 | Paper |
| Safe recursion with higher types and BCK-algebra | 2000-09-04 | Paper |
| An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras | 2000-02-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4247303 | 2000-02-15 | Paper |
| A new method for establishing conservativity of classical systems over their intuitionistic version | 1999-11-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4225149 | 1999-01-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4218937 | 1998-11-15 | Paper |
| On behavioural abstraction and behavioural satisfaction in higher-order logic | 1997-02-27 | Paper |
| Sound and complete axiomatisations of call-by-value control operators | 1996-07-15 | Paper |
| Positive subtyping | 1996-07-03 | Paper |
