| Publication | Date of Publication | Type |
|---|
| Designing a safe forward chaining tactic using productive proofs | 2026-02-10 | Paper |
| Formal Reasoning Using Distributed Assertions | 2024-05-03 | Paper |
| Undecidability of multiplicative subexponential logic | 2021-12-06 | Paper |
Undecidability of multiplicative subexponential logic
(available as arXiv preprint) | 2021-12-06 | Paper |
| Subformula linking for intuitionistic logic with application to type theory | 2021-12-01 | Paper |
Hybrid linear logic, revisited
Mathematical Structures in Computer Science | 2019-10-09 | Paper |
| Abella: a system for reasoning about relational specifications | 2019-09-18 | Paper |
Expressing additives using multiplicatives and subexponentials
Mathematical Structures in Computer Science | 2018-04-25 | Paper |
Equality and fixpoints in the calculus of structures
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) | 2018-04-23 | Paper |
| Modular focused proof systems for intuitionistic modal logics | 2017-10-17 | Paper |
| A proof-theoretic characterization of independence in type theory | 2017-07-12 | Paper |
| A two-level logic approach to reasoning about typed specification languages | 2017-04-25 | Paper |
A hybrid linear logic for constrained transition systems
(available as arXiv preprint) | 2017-03-13 | Paper |
A multi-focused proof system isomorphic to expansion proofs
Journal Of Logic And Computation | 2016-07-07 | Paper |
Focused and Synthetic Nested Sequents
Lecture Notes in Computer Science | 2016-06-10 | Paper |
An adequate compositional encoding of bigraph structure in linear logic with subexponentials
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Disproving using the inverse method by iterative refinement of finite approximations
Lecture Notes in Computer Science | 2015-12-11 | Paper |
Subformula Linking as an Interaction Method
Interactive Theorem Proving | 2013-08-07 | Paper |
Compact proof certificates for linear logic
Certified Programs and Proofs | 2013-04-19 | Paper |
| A systematic approach to canonicity in the classical sequent calculus | 2012-11-22 | Paper |
| The focused calculus of structures | 2012-09-18 | Paper |
Magically constraining the inverse method using dynamic polarity assignment
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
Classical and intuitionistic subexponential logics are equally expressive
Computer Science Logic | 2010-09-03 | Paper |
A Logical Characterization of Forward and Backward Chaining in the Inverse Method
Automated Reasoning | 2009-03-12 | Paper |
Focusing Strategies in the Sequent Calculus of Synthetic Connectives
Logic for Programming, Artificial Intelligence, and Reasoning | 2009-01-27 | Paper |
A logical characterization of forward and backward chaining in the inverse method
Journal of Automated Reasoning | 2008-06-11 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Automated Deduction – CADE-20
Lecture Notes in Computer Science | 2006-11-01 | Paper |
