| 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 Programming Languages and Systems | 2023-07-25 | Paper |
| An improved general E-unification method | 2023-04-28 | Paper |
Solving simplification ordering constraints Constraints in Computational Logics | 2022-08-16 | Paper |
scientific article; zbMATH DE number 7471683 (Why is no real title available?) (available as arXiv preprint) | 2022-02-09 | Paper |
| scientific article; zbMATH DE number 7471683 (Why is no real title available?) | 2022-02-09 | Paper |
| Parametricity for primitive nested types | 2021-10-18 | Paper |
A general framework for relational parametricity Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
| Deep induction: induction rules for (truly) nested types | 2020-09-23 | Paper |
Local presentability of certain comma categories Applied Categorical Structures | 2020-03-05 | Paper |
Unification in an extensional lambda calculus with ordered function sorts and constant overloading Automated Deduction — CADE-12 | 2020-01-21 | Paper |
| Structural resolution for logic programming | 2019-04-24 | Paper |
Structural resolution for logic programming (available as arXiv preprint) | 2019-04-24 | Paper |
| On local presentability of T/A | 2018-07-06 | Paper |
Interleaving data and effects Journal of Functional Programming | 2017-10-23 | Paper |
A productivity checker for logic programming (available as arXiv preprint) | 2017-10-13 | Paper |
Bifibrational functorial semantics of parametric polymorphism Electronic Notes in Theoretical Computer Science | 2016-12-16 | Paper |
Free theorems in the presence of seq Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-11-11 | Paper |
Monadic augment and generalised short cut fusion Proceedings of the tenth ACM SIGPLAN international conference on Functional programming | 2015-01-06 | Paper |
Abstraction and invariance for algebraically indexed types Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-11-27 | Paper |
Foundations for structured programming with GADTs Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
A relationally parametric model of dependent type theory Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Indexed induction and coinduction, fibrationally Logical Methods in Computer Science | 2013-09-06 | Paper |
Fusing logic and control with local transformations: an example optimization Electronic Notes in Theoretical Computer Science | 2013-07-24 | Paper |
Generic fibrational induction Logical Methods in Computer Science | 2012-07-03 | Paper |
Fibrational induction meets effects Foundations of Software Science and Computational Structures | 2012-06-22 | Paper |
Refining inductive types Logical Methods in Computer Science | 2012-06-11 | Paper |
Indexed induction and coinduction, fibrationally Algebra and Coalgebra in Computer Science | 2011-09-02 | Paper |
When Is a Type Refinement an Inductive Type? Foundations of Software Science and Computational Structures | 2011-05-19 | Paper |
Fibrational induction rules for initial algebras Computer Science Logic | 2010-09-03 | Paper |
A principled approach to programming with nested types in Haskell Higher-Order and Symbolic Computation | 2010-03-05 | Paper |
A family of syntactic logical relations for the semantics of Haskell-like languages Information and Computation | 2009-04-14 | Paper |
Initial Algebra Semantics Is Enough! Lecture Notes in Computer Science | 2009-03-10 | Paper |
Selective strictness and parametricity in structural operational semantics, inequationally Theoretical Computer Science | 2007-12-18 | Paper |
Monadic augment and generalised short cut fusion Journal of Functional Programming | 2007-11-22 | Paper |
| scientific article; zbMATH DE number 5033863 (Why is no real title available?) | 2006-06-19 | Paper |
On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi Mathematical Structures in Computer Science | 2005-05-06 | Paper |
Short cut fusion is correct Journal of Functional Programming | 2004-05-18 | Paper |
| scientific article; zbMATH DE number 2036330 (Why is no real title available?) | 2004-02-02 | Paper |
A generalization of short-cut fusion and its correctness proof Higher-Order and Symbolic Computation | 2003-05-11 | Paper |
Warm fusion in Stratego: A case study in generation of program transformation systems Annals of Mathematics and Artificial Intelligence | 2002-06-27 | Paper |
A combinatory logic approach to higher-order E-unification Theoretical Computer Science | 1997-02-28 | Paper |
| scientific article; zbMATH DE number 976352 (Why is no real title available?) | 1997-02-05 | Paper |
Normal forms in combinatory logic Notre Dame Journal of Formal Logic | 1996-01-30 | Paper |
An improved general \(E\)-unification method Journal of Symbolic Computation | 1993-01-17 | Paper |