| Publication | Date of Publication | Type |
|---|
| A logical framework for modelling breast cancer progression | 2023-10-20 | Paper |
| Encoding a dependent-type λ-calculus in a logic programming language | 2023-04-28 | Paper |
| A logic program for transforming sequent proofs to natural deduction proofs | 2022-11-26 | Paper |
| A Linear Logical Framework in Hybrid (Invited Talk) | 2022-07-18 | Paper |
| A focused linear logical framework and its application to metatheory of object logics | 2022-01-20 | Paper |
| Tactic theorem proving with refinement-tree proofs and metavariables | 2020-01-21 | Paper |
| Formal meta-level analysis framework for quantum programming languages | 2019-11-12 | Paper |
| Formalizing abstract computability: Turing categories in Coq | 2019-11-12 | Paper |
| Formalization of metatheory of the Quipper quantum programming language in a linear logic | 2019-10-25 | Paper |
| Hybrid interactive theorem proving using nuprl and HOL | 2019-10-01 | Paper |
| Proof search with set variable instantiation in the Calculus of Constructions | 2019-01-15 | Paper |
| Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions | 2018-10-19 | Paper |
| The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey | 2016-05-26 | Paper |
| A Logical Framework for Systems Biology | 2015-08-06 | Paper |
| A semantic model of types and machine instructions for proof-carrying code | 2015-03-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2871875 | 2014-01-10 | Paper |
| Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax | 2012-07-31 | Paper |
| Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison | 2010-09-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3656423 | 2010-01-13 | Paper |
| Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq | 2009-03-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3593496 | 2007-07-20 | Paper |
| Term Rewriting and Applications | 2005-11-11 | Paper |
| Typed Lambda Calculi and Applications | 2005-11-11 | Paper |
| Typed Lambda Calculi and Applications | 2005-11-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3024831 | 2005-07-04 | Paper |
| Dependent types ensure partial correctness of theorem provers | 2004-09-27 | Paper |
| Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf | 2004-09-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4406017 | 2003-06-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4484341 | 2003-06-12 | Paper |
| Current trends in logical frameworks and metalanguages | 2003-02-16 | Paper |
| The calculus of constructions as a framework for proof search with set variable instantiation | 2000-08-23 | Paper |
| Cache coherency in SCI: Specification and a sketch of correctness | 2000-05-09 | Paper |
| Interactive theorem proving with temporal logic | 1997-10-13 | Paper |
| Implementing tactics and tacticals in a higher-order logic programming language | 1994-01-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4012881 | 1992-09-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3789101 | 1988-01-01 | Paper |
