| Publication | Date of Publication | Type |
|---|
| Formal small-step verification of a call-by-value lambda calculus machine | 2023-08-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q6099607 | 2023-06-20 | Paper |
| A foundation for higher-order concurrent constraint programming | 2022-08-16 | Paper |
| A confluent relational calculus for higher-order programming with constraints | 2022-08-16 | Paper |
| A record calculus with principal types | 2022-08-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5111317 | 2020-05-26 | Paper |
| Call-by-value lambda calculus as a model of computation in Coq | 2019-08-21 | Paper |
| Categoricity results and large model constructions for second-order ZF in dependent type theory | 2019-08-21 | Paper |
| Verification of PCP-related computational reductions in Coq | 2018-10-04 | Paper |
| Regular language representations in the constructive type theory of Coq | 2018-08-21 | Paper |
| Weak call-by-value lambda calculus as a model of computation in Coq | 2018-01-04 | Paper |
| Categoricity results for second-order ZF in dependent type theory | 2018-01-04 | Paper |
| Tower Induction and Up-to Techniques for CCS with Fixed Points | 2017-07-21 | Paper |
| Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification | 2017-02-01 | Paper |
| Two-Way Automata in Coq | 2016-10-27 | Paper |
| Hereditarily Finite Sets in Constructive Type Theory | 2016-10-27 | Paper |
| Clausal Tableaux for Hybrid PDL | 2016-10-07 | Paper |
| Completeness and decidability results for CTL in constructive type theory | 2016-05-26 | Paper |
| A Linear First-Order Functional Intermediate Language for Verified Compilers | 2015-09-14 | Paper |
| Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions | 2015-09-14 | Paper |
| Transfinite Constructions in Classical Type Theory | 2015-09-14 | Paper |
| A goal-directed decision procedure for hybrid PDL | 2015-06-23 | Paper |
| Hybrid Tableaux for the Difference Modality | 2015-03-23 | Paper |
| A Constructive Theory of Regular Languages in Coq | 2015-01-13 | Paper |
| Completeness and Decidability Results for CTL in Coq | 2014-09-08 | Paper |
| Higher-Order Syntax and Saturation Algorithms for Hybrid Logic | 2013-12-20 | Paper |
| Constructive Completeness for Modal Logic with Transitive Closure | 2013-04-19 | Paper |
| Programmierung – eine Einführung in die Informatik mit Standard ML | 2011-12-02 | Paper |
| Constructive Formalization of Hybrid Logic with Eventualities | 2011-11-22 | Paper |
| Programmierung – eine Einführung in die Informatik mit Standard ML | 2011-09-22 | Paper |
| Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics | 2011-07-01 | Paper |
| Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies | 2011-05-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086781 | 2011-03-30 | Paper |
| Terminating Tableaux for $\mathcal{SOQ}$ with Number Restrictions on Transitive Roles | 2010-10-27 | Paper |
| Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference | 2010-10-12 | Paper |
| Terminating Tableaux for Hybrid Logic with Eventualities | 2010-09-14 | Paper |
| Analytic Tableaux for Simple Type Theory and its First-Order Fragment | 2010-07-27 | Paper |
| Terminating tableau systems for hybrid logic with difference and converse | 2010-01-06 | Paper |
| Terminating Tableaux for the Basic Fragment of Simple Type Theory | 2009-12-01 | Paper |
| Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies | 2009-12-01 | Paper |
| Extended First-Order Logic | 2009-10-20 | Paper |
| Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse | 2008-11-27 | Paper |
| Generating Propagators for Finite Set Constraints | 2008-09-09 | Paper |
| A concurrent lambda calculus with futures | 2007-01-09 | Paper |
| Frontiers of Combining Systems | 2006-10-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4227021 | 1999-10-25 | Paper |
| Situated simplification | 1998-07-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4364535 | 1997-11-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4364536 | 1997-11-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5688930 | 1997-05-25 | Paper |
| A complete and recursive feature theory | 1997-02-28 | Paper |
| A feature constraint system for logic programming with entailment | 1994-11-29 | Paper |
| Records for logic programming | 1994-05-05 | Paper |
| On the expressivity of feature logics with negation, functional uncertainty, and sort equations | 1994-03-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3995237 | 1993-01-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4013976 | 1992-09-27 | Paper |
| Feature-constraint logics for unification grammars | 1992-08-13 | Paper |
| Attributive concept descriptions with complements | 1991-01-01 | Paper |
| Order-sorted unification | 1989-01-01 | Paper |
| Inheritance hierarchies: Semantics and unifications | 1989-01-01 | Paper |
| Basic narrowing revisited | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3490936 | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3965577 | 1982-01-01 | Paper |
