| Publication | Date of Publication | Type |
|---|
| GADTs, functoriality, parametricity: pick two | 2025-01-13 | Paper |
| Higher-kinded data types. Syntax and semantics | 2024-12-19 | Paper |
| Characterizing functions mappable over GADTs | 2023-07-25 | Paper |
| An improved general E-unification method | 2023-04-28 | Paper |
| Solving simplification ordering constraints | 2022-08-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5028445 | 2022-02-09 | Paper |
| Parametricity for primitive nested types | 2021-10-18 | Paper |
| A General Framework for Relational Parametricity | 2021-01-20 | Paper |
| Deep induction: induction rules for (truly) nested types | 2020-09-23 | Paper |
| Local presentability of certain comma categories | 2020-03-05 | Paper |
| Unification in an extensional lambda calculus with ordered function sorts and constant overloading | 2020-01-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4631184 | 2019-04-24 | Paper |
| On local presentability of T/A | 2018-07-06 | Paper |
| Interleaving data and effects | 2017-10-23 | Paper |
| A productivity checker for logic programming | 2017-10-13 | Paper |
| Bifibrational functorial semantics of parametric polymorphism | 2016-12-16 | Paper |
| Free theorems in the presence of seq | 2015-11-11 | Paper |
| Monadic augment and generalised short cut fusion | 2015-01-06 | Paper |
| Abstraction and invariance for algebraically indexed types | 2014-11-27 | Paper |
| Foundations for structured programming with GADTs | 2014-09-12 | Paper |
| A relationally parametric model of dependent type theory | 2014-04-10 | Paper |
| Indexed induction and coinduction, fibrationally | 2013-09-06 | Paper |
| Fusing logic and control with local transformations: an example optimization | 2013-07-24 | Paper |
| Generic fibrational induction | 2012-07-03 | Paper |
| Fibrational Induction Meets Effects | 2012-06-22 | Paper |
| Refining inductive types | 2012-06-11 | Paper |
| Indexed Induction and Coinduction, Fibrationally | 2011-09-02 | Paper |
| When Is a Type Refinement an Inductive Type? | 2011-05-19 | Paper |
| Fibrational Induction Rules for Initial Algebras | 2010-09-03 | Paper |
| A principled approach to programming with nested types in Haskell | 2010-03-05 | Paper |
| A family of syntactic logical relations for the semantics of Haskell-like languages | 2009-04-14 | Paper |
| Initial Algebra Semantics Is Enough! | 2009-03-10 | Paper |
| Selective strictness and parametricity in structural operational semantics, inequationally | 2007-12-18 | Paper |
| Monadic augment and generalised short cut fusion | 2007-11-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5472909 | 2006-06-19 | Paper |
| On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi | 2005-05-06 | Paper |
| Short cut fusion is correct | 2004-05-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4445767 | 2004-02-02 | Paper |
| A generalization of short-cut fusion and its correctness proof | 2003-05-11 | Paper |
| Warm fusion in Stratego: A case study in generation of program transformation systems | 2002-06-27 | Paper |
| A combinatory logic approach to higher-order E-unification | 1997-02-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4331757 | 1997-02-05 | Paper |
| Normal forms in combinatory logic | 1996-01-30 | Paper |
| An improved general \(E\)-unification method | 1993-01-17 | Paper |
