| Publication | Date of Publication | Type |
|---|
| Integrating cost and behavior in type theory (invited talk) | 2024-11-26 | Paper |
| Amortized analysis via coinduction (early ideas) | 2024-11-26 | Paper |
| Sheaf semantics of termination-insensitive noninterference | 2024-05-27 | Paper |
| Internal Parametricity for Cubical Type Theory | 2023-02-07 | Paper |
| Logical Relations as Types: Proof-Relevant Parametricity for Program Modules | 2022-12-08 | Paper |
| Logic representation in LF | 2022-08-16 | Paper |
| Cartesian cubical computational type theory: Constructive reasoning with paths and equalities | 2022-05-28 | Paper |
| Internal parametricity for cubical type theory | 2022-02-09 | Paper |
| Syntax and models of Cartesian cubical type theory | 2022-01-20 | Paper |
| An Equational Logical Framework for Type Theories | 2021-06-02 | Paper |
| Guarded computational type theory | 2021-01-20 | Paper |
| Verified tail bounds for randomized programs | 2018-10-04 | Paper |
| Exception tracking in an open world | 2018-07-26 | Paper |
| Meaning explanations at higher dimension | 2018-01-12 | Paper |
| Correctness of compiling polymorphism to dynamic typing | 2017-10-23 | Paper |
| Homotopical patch theory | 2017-10-23 | Paper |
| Computational higher-dimensional type theory | 2017-10-20 | Paper |
| Parallel functional arrays | 2017-10-20 | Paper |
| Extensional equivalence and singleton types | 2017-07-12 | Paper |
| On equivalence and canonical forms in the LF type theory | 2017-07-12 | Paper |
| A higher-order logic for concurrent termination-preserving refinement | 2017-05-19 | Paper |
| Homotopical patch theory | 2016-09-29 | Paper |
| 2-Dimensional Directed Type Theory | 2016-07-15 | Paper |
| Practical foundations for programming languages | 2016-05-11 | Paper |
| Canonicity for 2-dimensional type theory | 2015-09-11 | Paper |
| A type system for higher-order modules | 2015-09-11 | Paper |
| A type theory for memory allocation and data layout | 2015-09-11 | Paper |
| Dynamizing static algorithms, with applications to dynamic trees and history independence | 2015-08-03 | Paper |
| Deciding type equivalence in a language with singleton kinds | 2015-03-17 | Paper |
| Adaptive functional programming | 2015-03-17 | Paper |
| Space profiling for parallel functional programs | 2015-03-16 | Paper |
| Automatic generation of staged geometric predicates | 2015-03-09 | Paper |
| A dependently typed assembly language | 2015-03-09 | Paper |
| A Note on the Uniform Kan Condition in Nominal Cubical Sets | 2015-01-22 | Paper |
| A universe of binding and computation | 2015-01-06 | Paper |
| Towards a mechanized metatheory of Standard ML | 2014-09-12 | Paper |
| Modular type classes | 2014-09-12 | Paper |
| Syntactic logical relations for polymorphic and recursive types | 2013-12-06 | Paper |
| Space profiling for parallel functional programs | 2011-07-25 | Paper |
| Mechanizing metatheory in a logical framework | 2007-09-26 | Paper |
| Computer Science Logic | 2006-11-01 | Paper |
| Automata, Languages and Programming | 2005-08-24 | Paper |
| Corrigendum: Polymorphic type assignment and CPS conversion | 2004-03-15 | Paper |
| Automatic generation of staged geometric predicates | 2004-03-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4420573 | 2003-08-18 | Paper |
| Relational interpretations of recursive types in an operational setting. | 2003-01-14 | Paper |
| Parametricity and variants of Girard's \(J\) operator | 2002-07-25 | Paper |
| Persistent triangulations | 2001-11-21 | Paper |
| On the unusual effectiveness of logic in computer science | 2001-09-10 | Paper |
| Semantics of memory management for polymorphic languages | 2001-07-08 | Paper |
| Proof-directed debugging | 2000-03-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4222944 | 1999-01-06 | Paper |
| A module system for a programming language based on the LF logical framework | 1998-07-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4364397 | 1997-11-17 | Paper |
| A note on ``A simplified account of polymorphic references | 1997-02-27 | Paper |
| Operational interpretations of an extension of Fω with control operators | 1996-12-16 | Paper |
| Structured theory presentations and logic representations | 1995-03-29 | Paper |
| A simplified account of polymorphic references | 1994-09-25 | Paper |
| A framework for defining logics | 1993-05-16 | Paper |
| Constructing type systems over an operational semantics | 1993-01-16 | Paper |
| Type checking with universes | 1992-06-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3204067 | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4721631 | 1987-01-01 | Paper |
| Amortized Analysis via Coalgebra | N/A | Paper |
