| Publication | Date of Publication | Type |
|---|
| Focusing Gentzen's LK proof system | 2024-10-01 | Paper |
| Formal Reasoning Using Distributed Assertions | 2024-05-03 | Paper |
| Encoding a dependent-type λ-calculus in a logic programming language | 2023-04-28 | Paper |
| Functions-as-constructors higher-order unification: extended pattern unification | 2022-05-04 | Paper |
| From axioms to synthetic inference rules via focusing | 2022-04-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5014803 | 2021-12-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4992520 | 2021-06-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5858725 | 2021-04-14 | Paper |
| A proof theory for model checking | 2019-10-25 | Paper |
| Abella: A System for Reasoning about Relational Specifications | 2019-09-18 | Paper |
| Mechanized metatheory revisited | 2019-09-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4619819 | 2019-02-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4636050 | 2018-04-23 | Paper |
| Proof certificates for equality reasoning | 2018-04-23 | Paper |
| A semantic framework for proof evidence | 2018-02-22 | Paper |
| Functions-as-constructors Higher-order Unification | 2017-10-17 | Paper |
| Translating between implicit and explicit versions of proof | 2017-09-22 | Paper |
| A proof theory for generic judgments | 2017-07-12 | Paper |
| Unifying Classical and Intuitionistic Logics for Computational Control | 2017-07-03 | Paper |
| Reasoning with higher-order abstract syntax in a logical framework | 2017-06-13 | Paper |
| Preserving differential privacy under finite-precision semantics | 2017-02-06 | Paper |
| A multi-focused proof system isomorphic to expansion proofs | 2016-07-07 | Paper |
| Reasoning in Abella about structural operational semantics specifications | 2016-05-06 | Paper |
| Focused Labeled Proof Systems for Modal Logic | 2016-01-12 | Paper |
| On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control | 2016-01-12 | Paper |
| Least and Greatest Fixed Points in Linear Logic | 2015-09-17 | Paper |
| Proof search specifications of bisimulation and modal logics for the π-calculus | 2015-09-17 | Paper |
| Formalizing Operational Semantic Specifications in Logic | 2015-04-09 | Paper |
| Extracting Proofs from Tabled Proof Search | 2015-01-13 | Paper |
| A game semantics for proof search (preliminary results) | 2013-10-08 | Paper |
| A congruence format for name-passing calculi | 2013-10-07 | Paper |
| A proof search specification of the \(\pi\)-calculus | 2013-09-26 | Paper |
| A two-level logic approach to reasoning about computations | 2013-08-01 | Paper |
| Encoding generic judgments: preliminary results | 2013-07-24 | Paper |
| Foundational proof certificates in first-order logic | 2013-06-14 | Paper |
| A formal framework for specifying sequent calculus proof systems | 2013-03-27 | Paper |
| Kripke semantics and proof systems for combining intuitionistic logic and classical logic | 2012-11-29 | Paper |
| A systematic approach to canonicity in the classical sequent calculus | 2012-11-22 | Paper |
| Programming with higher-order logic. | 2012-06-15 | Paper |
| A proposal for broad spectrum proof certificates | 2011-11-22 | Paper |
| A focused approach to combining logics | 2011-09-22 | Paper |
| Proof and refutation in MALL as a game | 2011-08-26 | Paper |
| Nominal abstraction | 2011-01-13 | Paper |
| A framework for proof systems | 2010-10-08 | Paper |
| Focused Inductive Theorem Proving | 2010-09-14 | Paper |
| Focusing and polarization in linear, intuitionistic, and classical logics | 2009-11-04 | Paper |
| Incorporating Tables into Proofs | 2009-03-05 | Paper |
| From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic | 2009-03-05 | Paper |
| Focusing and Polarization in Intuitionistic Logic | 2009-03-05 | Paper |
| Focusing in Linear Meta-logic | 2008-11-27 | Paper |
| On the Specification of Sequent Systems | 2008-05-27 | Paper |
| Least and Greatest Fixed Points in Linear Logic | 2008-05-15 | Paper |
| Computer Science Logic | 2005-08-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4664255 | 2005-04-05 | Paper |
| Encoding transition systems in sequent calculus | 2003-07-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4415240 | 2003-07-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4412848 | 2003-07-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4537502 | 2002-07-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2767057 | 2002-01-28 | Paper |
| Cut-elimination for a logic with definitions and induction | 2000-08-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4222839 | 1998-12-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4391451 | 1998-06-03 | Paper |
| Forum: A multiple-conclusion specification logic | 1997-02-27 | Paper |
| From operational semantics to abstract machines | 1994-10-31 | Paper |
| Logic programming in a fragment of intuitionistic linear logic | 1994-07-18 | Paper |
| Uniform proofs as a foundation for logic programming | 1991-01-01 | Paper |
| Higher-order Horn clauses | 1990-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3789101 | 1988-01-01 | Paper |
| A compact representation of proofs | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3751042 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3343471 | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3338232 | 1984-01-01 | Paper |
