| Publication | Date of Publication | Type |
|---|
| A toy model provably featuring an arrow of time without past hypothesis | 2024-11-13 | Paper |
| From rewrite rules to axioms in the \(\lambda \varPi \)-calculus modulo theory | 2024-10-30 | Paper |
| Theoretical computer science: computability, decidability and logic | 2024-09-11 | Paper |
| Theoretical computer science: computational complexity | 2024-09-11 | Paper |
| Linear lambda-calculus is linear | 2024-05-27 | Paper |
| Extensional proofs in a propositional logic modulo isomorphisms | 2023-10-17 | Paper |
| Some Axioms for Mathematics | 2023-06-23 | Paper |
| A toy model provably featuring an arrow of time without past hypothesis | 2023-06-12 | Paper |
| A new connective in natural deduction, and its application to quantum computing | 2023-04-27 | Paper |
| A modular construction of type theories | 2023-03-22 | Paper |
| Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs | 2023-02-28 | Paper |
| Typing Quantum Superpositions and Measurement | 2022-12-09 | Paper |
| From the universality of mathematical truth to the interoperability of proof systems | 2022-12-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5089014 | 2022-07-18 | Paper |
| A new connective in natural deduction, and its application to quantum computing | 2022-03-31 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5013815 | 2021-12-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4994968 | 2021-06-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4992399 | 2021-06-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5150132 | 2021-02-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5123182 | 2020-09-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5111441 | 2020-05-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5219928 | 2020-03-09 | Paper |
| The Age of Algorithms | 2019-12-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3119364 | 2019-03-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2980972 | 2017-05-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2980113 | 2017-04-27 | Paper |
| A Completion Method to Decide Reachability in Rewrite Systems | 2017-02-27 | Paper |
| Yet another bijection between sequent calculus and natural deduction | 2016-08-01 | Paper |
| A calculus for automatic verification of Petri nets based on resolution and dynamic logics | 2016-08-01 | Paper |
| The physical Church thesis as an explanation of the Galileo thesis | 2016-07-08 | Paper |
| Universality in two dimensions | 2016-04-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3463667 | 2016-01-19 | Paper |
| Decidability, Introduction Rules and Automata | 2016-01-12 | Paper |
| Permissive-nominal logic | 2015-09-17 | Paper |
| The physical Church–Turing thesis and non-deterministic computation over the real numbers | 2015-08-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4983482 | 2015-03-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5412237 | 2014-04-25 | Paper |
| On the convergence of reduction-based and model-based methods in proof theory | 2013-12-13 | Paper |
| A computational definition of the notion of vectorial space | 2013-09-20 | Paper |
| Real Numbers, Chaos, and the Principle of a Bounded Density of Information | 2013-06-14 | Paper |
| Causal graph dynamics | 2013-06-06 | Paper |
| Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic | 2013-06-06 | Paper |
| THE PHYSICAL CHURCH-TURING THESIS AND THE PRINCIPLES OF QUANTUM THEORY | 2013-01-18 | Paper |
| A simple proof that super-consistency implies cut elimination | 2012-11-29 | Paper |
| Causal Graph Dynamics | 2012-11-01 | Paper |
| A Theory Independent Curry-De Bruijn-Howard Correspondence | 2012-11-01 | Paper |
| PNL to HOL: from the logic of nominal sets to the logic of higher-order functions | 2012-10-11 | Paper |
| Provably correct conflict prevention bands algorithms | 2012-07-20 | Paper |
| Around the Physical Church-Turing Thesis: Cellular Automata, Formal Languages, and the Principles of Quantum Theory | 2012-06-08 | Paper |
| A formal library of set relations and its application to synchronous languages | 2011-12-23 | Paper |
| On the expressive power of schemes | 2011-10-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086782 | 2011-03-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3083673 | 2011-03-23 | Paper |
| Proofs and algorithms. An introduction to logic and computability | 2011-02-15 | Paper |
| Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques | 2010-12-14 | Paper |
| Polarized Resolution Modulo | 2010-10-27 | Paper |
| Introduction to the theory of programming languages. | 2010-10-13 | Paper |
| On the Completeness of Quantum Computation Models | 2010-07-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3571945 | 2010-06-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3571944 | 2010-06-29 | Paper |
| On the convergence of reduction-based and model-based methods in proof theory | 2009-11-12 | Paper |
| Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo | 2009-03-10 | Paper |
| Truth Values Algebras and Proof Normalization | 2009-03-10 | Paper |
| The metamorphoses of the calculus. An amazing history of mathematics | 2008-11-10 | Paper |
| Principles of programming languages | 2008-10-02 | Paper |
| Linear-algebraic λ-calculus: higher-order, encodings, and confluence. | 2008-08-28 | Paper |
| Type theory and proof processing systems | 2008-02-08 | Paper |
| Introduction to proof theory | 2008-01-14 | Paper |
| A Simple Proof That Super-Consistency Implies Cut Elimination | 2008-01-02 | Paper |
| Automated Deduction – CADE-20 | 2006-11-01 | Paper |
| Eigenvariables, bracketing and the decidability of positive minimal predicate logic | 2006-09-14 | Paper |
| Term Rewriting and Applications | 2005-11-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3024833 | 2005-07-04 | Paper |
| Proof normalization modulo | 2005-02-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4736827 | 2004-08-11 | Paper |
| Theorem proving modulo | 2004-05-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4447217 | 2004-02-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4428296 | 2003-09-15 | Paper |
| Higher order unification via explicit substitutions | 2003-01-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4787249 | 2003-01-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3149664 | 2002-09-30 | Paper |
| Higher-order unification and matching | 2002-08-27 | Paper |
| About folding-unfolding cuts and cuts modulo | 2002-06-06 | Paper |
| HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic | 2001-11-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4518864 | 2000-12-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4944850 | 2000-09-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4503899 | 2000-09-14 | Paper |
| Collections, sets and types | 2000-06-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4938612 | 2000-04-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4246945 | 1999-06-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4365102 | 1999-02-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4871733 | 1996-04-02 | Paper |
| Third order matching is decidable | 1994-11-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4303686 | 1994-10-23 | Paper |
| A Complete Proof Synthesis Method for the Cube of Type Systems | 1994-06-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4281470 | 1994-06-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4035236 | 1993-05-18 | Paper |
| The undecidability of pattern matching in calculi where primitive recursive functions are representable | 1993-05-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3986688 | 1992-06-27 | Paper |
| A linear proof language for second-order intuitionistic linear logic | N/A | Paper |
