| Publication | Date of Publication | Type |
|---|
| Conservativity between logics and typed λ calculi | 2023-12-08 | Paper |
| A short and flexible proof of strong normalization for the calculus of constructions | 2023-12-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q6060674 | 2023-11-03 | Paper |
| Apartness and distinguishing formulas in Hennessy-Milner logic | 2023-07-26 | Paper |
| Characteristics of de Bruijn’s early proof checker Automath | 2022-07-14 | Paper |
| The construction of set-truncated higher inductive types | 2022-04-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5155676 | 2021-10-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4957790 | 2021-09-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4995377 | 2021-06-24 | Paper |
| The Tactician. A seamless, interactive tactic learner and prover for Coq | 2021-01-20 | Paper |
| Strong Normalization for Truth Table Natural Deduction | 2020-01-24 | Paper |
| Deriving Natural Deduction Rules from Truth Tables | 2019-07-24 | Paper |
| Modular properties of algebraic type systems | 2019-01-11 | Paper |
| Type Theory based on Dependent Inductive and Coinductive Types | 2018-04-23 | Paper |
| A formalisation of consistent consequence for Boolean equation systems | 2018-01-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2988060 | 2017-05-18 | Paper |
| Type Theory and Formal Proof | 2014-10-22 | Paper |
| N. G. de Bruijn's contribution to the formalization of mathematics | 2014-09-03 | Paper |
| Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description | 2014-08-07 | Paper |
| Deduction Graphs with Universal Quantification | 2014-01-17 | Paper |
| A Logical Framework with Explicit Conversions | 2014-01-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2847396 | 2013-09-09 | Paper |
| Formal Mathematics on Display: A Wiki for Flyspeck | 2013-08-09 | Paper |
| Communicating Formal Proofs: The Case of Flyspeck | 2013-08-07 | Paper |
| The \(\lambda \mu^{\mathbf{T}}\)-calculus | 2013-04-15 | Paper |
| Learning2Reason | 2011-07-29 | Paper |
| The correctness of Newman's typability algorithm and some of its extensions | 2011-07-07 | Paper |
| Levels of undecidability in rewriting | 2011-02-21 | Paper |
| Automated Machine-Checked Hybrid System Safety Proofs | 2010-09-14 | Paper |
| Proviola: A Tool for Proof Re-animation | 2010-08-24 | Paper |
| A Wiki for Mizar: Motivation, Considerations, and Initial Prototype | 2010-08-24 | Paper |
| Proof assistants: history, ideas and future | 2009-11-23 | Paper |
| Degrees of Undecidability in Term Rewriting | 2009-11-12 | Paper |
| Social processes, program verification and all that | 2009-11-11 | Paper |
| Introduction to Type Theory | 2009-07-28 | Paper |
| A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$ | 2009-07-09 | Paper |
| Rewriting Techniques and Applications | 2009-04-30 | Paper |
| (In)consistency of Extensions of Higher Order Logic and Type Theory | 2009-03-10 | Paper |
| Natural deduction via graphs: formal definition and computation rules | 2007-09-26 | Paper |
| From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions | 2007-09-05 | Paper |
| Constructive analysis, types and exact real numbers | 2007-04-12 | Paper |
| Mathematical Knowledge Management | 2007-02-12 | Paper |
| Mathematical Knowledge Management | 2005-08-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4736391 | 2004-08-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4736392 | 2004-08-09 | Paper |
| A constructive algebraic hierarchy in Coq. | 2003-08-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4411846 | 2003-07-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2778821 | 2002-03-21 | Paper |
| Proof by computation in the Coq system | 2002-03-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2767915 | 2002-02-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2751370 | 2001-12-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2754042 | 2001-11-11 | Paper |
| Some logical and syntactical observations concerning the first-order dependent type system λP | 2000-06-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4945243 | 2000-06-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4939698 | 2000-02-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4703134 | 1999-12-14 | Paper |
| Modularity of strong normalization in the algebraic-λ-cube | 1999-03-16 | Paper |
| Explicit substitution. On the edge of strong normalization | 1999-01-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4362916 | 1997-11-13 | Paper |
