| Publication | Date of Publication | Type |
|---|
| Towards semantic markup of mathematical documents via user interaction | 2024-12-04 | Paper |
| Isabelle/HOL/GST: a formal proof environment for generalized set theories | 2023-06-02 | Paper |
| Generating custom set theories with non-set structured objects | 2022-04-22 | Paper |
| Adding an abstraction barrier to ZF set theory | 2021-01-20 | Paper |
| BNF-style notation as it is actually used | 2020-01-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4619823 | 2019-02-07 | Paper |
| Strongly typed flow-directed representation transformations (extended abstract) | 2017-08-21 | Paper |
| Skalpel: a constraint-based type error slicer for standard ML | 2017-02-06 | Paper |
| Bridging Curry and Church's typing style | 2016-10-31 | Paper |
| Automath Type Inclusion in Barendregt’s Cube | 2015-10-20 | Paper |
| Functioning without closure | 2015-03-09 | Paper |
| Type inference, principal typings, and let-polymorphism for first-class mixin modules | 2015-01-06 | Paper |
| Computerizing mathematical text with MathLang | 2013-12-13 | Paper |
| Expansion: the crucial mechanism for type inference with intersection types: a survey and explanation | 2013-10-02 | Paper |
| MathLang: experience-driven development of a new mathematical language | 2013-09-09 | Paper |
| Implementing compositional analysis using intersection types with expansion variables | 2013-08-16 | Paper |
| On Realisability Semantics for Intersection Types with Expansion Variables | 2013-01-24 | Paper |
| Reducibility Proofs in the λ-Calculus | 2013-01-24 | Paper |
| The Algebra of Expansion | 2013-01-24 | Paper |
| Expansion for Universal Quantifiers | 2012-06-22 | Paper |
| Compilation of extended recursion in call-by-value functional languages | 2010-03-05 | Paper |
| MathLang Translation to Isabelle Syntax | 2009-07-09 | Paper |
| Realisability Semantics for Intersection Types and Expansion Variables | 2009-05-13 | Paper |
| A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables | 2009-01-27 | Paper |
| Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis | 2008-04-24 | Paper |
| Restoring Natural Language as a Computerised Mathematics Input Method | 2007-11-28 | Paper |
| Narrative Structure of Mathematical Texts | 2007-11-28 | Paper |
| Programming Languages and Systems | 2007-09-28 | Paper |
| Programming Languages and Systems | 2007-09-28 | Paper |
| Mathematical Knowledge Management | 2007-02-12 | Paper |
| Programming Languages and Systems | 2005-09-13 | Paper |
| Mathematical Knowledge Management | 2005-08-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4673435 | 2005-04-29 | Paper |
| Type error slicing in implicitly typed higher-order languages | 2004-11-22 | Paper |
| Principality and type inference for intersection types using expansion variables | 2004-10-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4737219 | 2004-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4738350 | 2004-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4447225 | 2004-02-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4417900 | 2003-07-30 | Paper |
| A calculus with polymorphic and polyvariant flow types | 2002-10-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4532090 | 2002-05-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4518890 | 2001-05-20 | Paper |
| Cut rules and explicit substitutions | 2001-05-07 | Paper |
| Typability and type checking in System F are equivalent and undecidable | 1999-09-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4259970 | 1999-09-09 | Paper |
| Intersection Types via Finite-Set Declarations | N/A | Paper |
