| Publication | Date of Publication | Type |
|---|
| Towards semantic markup of mathematical documents via user interaction | 2024-12-04 | Paper |
| Introduction | 2024-09-06 | Paper |
| Substitution in the \(\lambda\)-calculus and the role of the Curry school | 2024-09-06 | Paper |
| A primer of mathematical analysis and the foundations of computation | 2024-03-01 | Paper |
| Thoughts on Using the History of Mathematics to Teach the Foundations of Mathematical Analysis | 2023-06-14 | 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 |
| Explicit substitution calculi with de Bruijn indices and intersection type systems | 2019-01-08 | 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 |
| The soundness of explicit substitution with nameless variables | 2015-04-29 | Paper |
| Simplified reducibility proofs of Church-Rosser for \({\beta}\)- and \({\beta}{\eta}\)-reduction | 2015-03-18 | Paper |
| A flexible framework for visualisation of computational properties of general explicit substitutions calculi | 2015-03-18 | Paper |
| Computerizing mathematical text with MathLang | 2013-12-13 | Paper |
| MathLang: experience-driven development of a new mathematical language | 2013-09-09 | Paper |
| Automath and Pure Type Systems | 2013-06-06 | Paper |
| Explicit substitutions à la de Bruijn: the local and global way | 2013-06-06 | Paper |
| Comparing calculi of explicit substitutions with eta-reduction | 2013-04-19 | Paper |
| On automating the extraction of programs from proofs using product types | 2013-04-19 | Paper |
| On realisability semantics for intersection types with expansion variables | 2013-01-24 | Paper |
| Reducibility Proofs in the λ-Calculus | 2013-01-24 | Paper |
| Russell's Orders in Kripke's Theory of Truth and Computational Type Theory | 2012-10-12 | Paper |
| On functions and types: a tutorial | 2011-04-01 | Paper |
| Intersection type system with de Bruijn indices | 2011-03-30 | Paper |
| Intersection type systems and explicit substitutions calculi | 2010-09-29 | Paper |
| Explicit substitutions calculi with one step eta-reduction decided explicitly | 2009-12-18 | Paper |
| SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi | 2009-11-30 | 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 |
| Principal Typings for Explicit Substitutions Calculi | 2008-06-19 | Paper |
| Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions | 2008-04-07 | Paper |
| The Weak Normalization of the Simply Typed se-calculus | 2008-01-14 | Paper |
| Restoring Natural Language as a Computerised Mathematics Input Method | 2007-11-28 | Paper |
| Narrative Structure of Mathematical Texts | 2007-11-28 | Paper |
| A completeness result for a realisability semantics for an intersection type system | 2007-05-23 | Paper |
| Mathematical Knowledge Management | 2007-02-12 | Paper |
| Logical reasoning. A first course | 2006-03-27 | Paper |
| Logic for Programming, Artificial Intelligence, and Reasoning | 2005-11-10 | Paper |
| Typed $\lambda$-calculi with one binder | 2005-10-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5693576 | 2005-09-26 | Paper |
| Mathematical Knowledge Management | 2005-08-26 | Paper |
| AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS | 2005-06-22 | Paper |
| Comparing and implementing calculi of explicit substitutions with eta-reduction | 2005-06-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4664921 | 2005-04-09 | Paper |
| De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case | 2005-02-22 | Paper |
| De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case | 2005-02-22 | Paper |
| A modern perspective on type theory. From its origins until today | 2004-11-25 | Paper |
| A refinement of de Bruijn's formal language of mathematics | 2004-08-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3044340 | 2004-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4447225 | 2004-02-16 | Paper |
| Formalizing Belief Revision in Type Theory | 2003-07-16 | Paper |
| Revisiting the notion of function | 2003-06-25 | Paper |
| Formalizing strong normalization proofs of explicit substitution calculi in ALF | 2003-06-09 | Paper |
| Pure Type Systems with de Bruijn Indices | 2002-12-19 | Paper |
| Unification via the \(\lambda s_e\)-style of explicit substitutions | 2002-06-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2763649 | 2002-01-21 | Paper |
| Reviewing the classical and the de Bruijn notation for \(\lambda\)-calculus and pure type systems | 2001-10-16 | Paper |
| Postponement, conservation and preservation of strong normalization for generalized reduction | 2001-10-03 | Paper |
| A correspondence between Martin-Löf type theory, the ramified theory of types and pure type systems | 2001-07-23 | Paper |
| Relating the - and s-styles of explicit substitutions | 2000-09-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4501582 | 2000-09-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4494365 | 2000-08-10 | Paper |
| On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations | 2000-02-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4259970 | 1999-09-09 | Paper |
| Bridging de Bruijn indices and variable names in explicit substitutions calculi | 1999-06-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4364376 | 1998-04-01 | Paper |
| Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms | 1998-03-12 | Paper |
| A useful \(\lambda\)-notation | 1997-09-09 | Paper |
| A unified approach to type theory through a refined \(\lambda\)-calculus | 1997-02-27 | Paper |
| Important Issues in Foundational Formalisms | 1997-01-13 | Paper |
| Canonical typing and ∏-conversion in the Barendregt Cube | 1996-11-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4877445 | 1996-07-16 | Paper |
| The Barendregt cube with definitions and generalised reduction | 1996-07-03 | Paper |
| Refining reduction in the lambda calculus | 1996-06-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4866983 | 1996-03-19 | Paper |
| A type free theory and collective/distributive predication | 1995-12-05 | Paper |
| ON STEPWISE EXPLICIT SUBSTITUTION | 1994-04-27 | Paper |
| Nominalization, predication and type containment | 1994-02-22 | Paper |
| \(\lambda\)-terms, logic, determiners and quantifiers | 1994-02-22 | Paper |
| Set Theory and Nominalization, Part II | 1993-08-23 | Paper |
| Set Theory and Nominalization, Part I | 1993-06-29 | Paper |
| A system at the cross-roads of functional and logic programming | 1993-05-16 | Paper |
| Intersection Types via Finite-Set Declarations | N/A | Paper |
