Collected Abstracts (PDF)
Proof Composition Mechanisms and Their Geometric Interpretation
Higher-order sequent proofs, higher-order nets
The proof equivalence problem for multiplicative linear logic is PSPACE-complete
Craig Interpolation, Proof-Theoretically via Nested Sequents
Reductive-free cyclic induction reasoning
First-order linear logic as a general framework for logic-based computational linguistics
Towards syntactic cut-elimination for temporal logics
Cyclic Abduction of Inductive Safety & Termination Preconditions
Construction of Bipolar Focussing Proof Structures
Extending the scope of labelled sequent calculi: the case of classical counterfactuals
Automating LPO Reasoning about Termination
Some ideas on bounded arithmetics for systems of monotone proofs
Proof Theory for Lattice-Ordered Groups
Interpolation in finitely-valued first-order logics
Linear Session Types for Solos
Curry-Howard for a lightweight interactive theorem prover
Toward a Theory of Contexts of Assumptions in Logical Frameworks
A Semantics for Proof Evidence
Type isomorphisms in presence of strong sums: axiomatizability, practical decidability and subtyping
Proofs in monoidal closed bifibrations
A classical theory of values and computations
Modelling canonical reasoning via unification hints (Do mathematicians learn prolog at kindergarden?)
A Coinductive Approach to Proof Search
Untyping Typed Algebraic Structures and Colouring Cyclic Linear Logic Proof Nets
Certifying formula-based induction reasoning
Defining new theories in SMT solvers using first-order axioms with triggers
Delayed instantiation of existential variables in presence of a theory
Implementing an interactive proof system