| 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
Annals of Mathematics and Artificial Intelligence | 2022-05-04 | Paper |
From axioms to synthetic inference rules via focusing
Annals of Pure and Applied Logic | 2022-04-01 | Paper |
A proof theory for model checking: an extended abstract
| 2021-12-08 | Paper |
Preserving differential privacy under finite-precision semantics
| 2021-06-09 | Paper |
A non-local method for robustness analysis of floating point programs
| 2021-04-14 | Paper |
A proof theory for model checking
Journal of Automated Reasoning | 2019-10-25 | Paper |
Abella: a system for reasoning about relational specifications
| 2019-09-18 | Paper |
Mechanized metatheory revisited
Journal of Automated Reasoning | 2019-09-02 | Paper |
scientific article; zbMATH DE number 7015113 (Why is no real title available?)
| 2019-02-07 | Paper |
scientific article; zbMATH DE number 6863660 (Why is no real title available?)
| 2018-04-23 | Paper |
Proof certificates for equality reasoning
| 2018-04-23 | Paper |
A semantic framework for proof evidence
Journal of Automated Reasoning | 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
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Unifying classical and intuitionistic logics for computational control
2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science | 2017-07-03 | Paper |
Reasoning with higher-order abstract syntax in a logical framework
ACM Transactions on Computational Logic | 2017-06-13 | Paper |
Preserving differential privacy under finite-precision semantics
Theoretical Computer Science | 2017-02-06 | Paper |
A multi-focused proof system isomorphic to expansion proofs
Journal Of Logic And Computation | 2016-07-07 | Paper |
Reasoning in Abella about structural operational semantics specifications
Electronic Notes in Theoretical Computer Science | 2016-05-06 | Paper |
Focused labeled proof systems for modal logic
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
On subexponentials, synthetic connectives, and multi-level delimited control
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Proof search specifications of bisimulation and modal logics for the \({\pi}\)-calculus
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Formalizing operational semantic specifications in logic
Electronic Notes in Theoretical Computer Science | 2015-04-09 | Paper |
Extracting proofs from tabled proof search
Certified Programs and Proofs | 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
Journal of Automated Reasoning | 2013-08-01 | Paper |
Encoding generic judgments: preliminary results
Electronic Notes in Theoretical Computer Science | 2013-07-24 | Paper |
Foundational proof certificates in first-order logic
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
A formal framework for specifying sequent calculus proof systems
Theoretical Computer Science | 2013-03-27 | Paper |
Kripke semantics and proof systems for combining intuitionistic logic and classical logic
Annals of Pure and Applied 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
Certified Programs and Proofs | 2011-11-22 | Paper |
A focused approach to combining logics
Annals of Pure and Applied Logic | 2011-09-22 | Paper |
Proof and refutation in MALL as a game
Annals of Pure and Applied Logic | 2011-08-26 | Paper |
Nominal abstraction
Information and Computation | 2011-01-13 | Paper |
A framework for proof systems
Journal of Automated Reasoning | 2010-10-08 | Paper |
Focused Inductive Theorem Proving
Automated Reasoning | 2010-09-14 | Paper |
Focusing and polarization in linear, intuitionistic, and classical logics
Theoretical Computer Science | 2009-11-04 | Paper |
Incorporating Tables into Proofs
Computer Science Logic | 2009-03-05 | Paper |
From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
Computer Science Logic | 2009-03-05 | Paper |
Focusing and Polarization in Intuitionistic Logic
Computer Science Logic | 2009-03-05 | Paper |
Focusing in Linear Meta-logic
Automated Reasoning | 2008-11-27 | Paper |
On the Specification of Sequent Systems
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Least and greatest fixed points in linear logic
Lecture Notes in Computer Science | 2008-05-15 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2005-08-22 | Paper |
scientific article; zbMATH DE number 2152687 (Why is no real title available?)
| 2005-04-05 | Paper |
Encoding transition systems in sequent calculus
Theoretical Computer Science | 2003-07-29 | Paper |
scientific article; zbMATH DE number 1954369 (Why is no real title available?)
| 2003-07-28 | Paper |
scientific article; zbMATH DE number 1950250 (Why is no real title available?)
| 2003-07-17 | Paper |
scientific article; zbMATH DE number 1761877 (Why is no real title available?)
| 2002-07-01 | Paper |
scientific article; zbMATH DE number 1696799 (Why is no real title available?)
| 2002-01-28 | Paper |
Cut-elimination for a logic with definitions and induction
Theoretical Computer Science | 2000-08-23 | Paper |
scientific article; zbMATH DE number 1231524 (Why is no real title available?)
| 1998-12-14 | Paper |
scientific article; zbMATH DE number 1158760 (Why is no real title available?)
| 1998-06-03 | Paper |
Forum: A multiple-conclusion specification logic
Theoretical Computer Science | 1997-02-27 | Paper |
From operational semantics to abstract machines
Mathematical Structures in Computer Science | 1994-10-31 | Paper |
Logic programming in a fragment of intuitionistic linear logic
Information and Computation | 1994-07-18 | Paper |
Uniform proofs as a foundation for logic programming
Annals of Pure and Applied Logic | 1991-01-01 | Paper |
Higher-order Horn clauses
Journal of the ACM | 1990-01-01 | Paper |
scientific article; zbMATH DE number 4053062 (Why is no real title available?)
| 1988-01-01 | Paper |
A compact representation of proofs
Studia Logica | 1987-01-01 | Paper |
scientific article; zbMATH DE number 3988745 (Why is no real title available?)
| 1986-01-01 | Paper |
scientific article; zbMATH DE number 3878393 (Why is no real title available?)
| 1984-01-01 | Paper |
scientific article; zbMATH DE number 3871341 (Why is no real title available?)
| 1984-01-01 | Paper |
