ABSTRACT. This will be a tutorial on deep inference for general computer scientists. It will connect with the simply-typed lambda-calculus, and with classical logic. No further background knowledge is expected.

ABSTRACT. It is possible to design proof systems for a vast range of logics, including all the common ones, by adopting two general proof constructors:

(1) the subatomic shape recently introduced by Andrea Aler Tubella, and

(2) a very general notion of formal substitution that is currently being explored by Benjamin Ralph and that subsumes standard quantification.

The two constructors could be considered two design principles, or, in other words, two ways of looking at proofs. In this talk, I will show how, by adopting them, we get a good starting point for designing proof systems that naturally yield canonical proofs of minimal size and that allow for a unified normalisation theory.

ABSTRACT. In this talk I shall make every effort to be provocative and controversial, in an attempt to fuel introspection at the 20 year mark of deep inference. The talk has three parts:

(1) Is deep inference "incoherent categorical logic"? Here "incoherent" refers to the omission of proof equality, covered by the coherence laws of categorical logic [1]. Is deep inference in danger of isolating itself as a community by not preserving the original language of categorical logic? Hilbert's 24th problem is on proof equality [2]; does deep inference short-change itself by not retaining proof equality as a first-class citizen, as it was in categorical logic?

(2) Linear distributivity (originally known as weak distributivity) [3] is core to the categorical approach to linear logic, hence also deep inference, where it has become known as switch. Classical logic follows with contraction and weakening. Combinatorial proofs [4] are an irredundant abstraction [2] of classical syntactic proofs, yet there is no natural interpretation of switch on combinatorial proofs, while there *is* a natural interpretation of sequent calculus conjunction. Could there be a deeper computational meaning to this, which reflects back on the standard switch-based formulations of deep inference for linear and classical logic?

(3) Extensions of combinatorial proofs. In part (2) I will have shown how easily one may translate a classical propositional syntactic proof into a combinatorial proof (literally a 30-second definition - I promise!). I will then talk about two extensions, where the translation from syntactic proofs is also very easy to explain to a lay audience: (a) intuitionistic combinatorial proofs (joint work with Heijltjes and Strassburger), and (b) classical first-order combinatorial proofs [5].

References and background reading:

[1] Deep inference proof theory equals categorical proof theory minus coherence. http://boole.stanford.edu/~dominic/papers/di/di.pdf

[2] Towards Hilbert's 24th problem: combinatorial proof invariants. http://boole.stanford.edu/~dominic/papers/invar/invar.pdf

[3] Robin Cockett, Robert Seely. Weakly Distributive Categories, JPAA 114 (1997)2. http://www.math.mcgill.ca/rags/linear/wdc.ps.gz

[4] Proofs without syntax. Annals of Mathematics, 164 (2006). http://annals.math.princeton.edu/wp-content/uploads/annals-v164-n3-p09.pdf

[5] First-order Proofs Without Syntax. Slides for the Berkeley Logic Colloquium, Oct. 17, 2014. http://boole.stanford.edu/~dominic/papers/fopws-blc-2014

ABSTRACT. In this talk I will survey the current state of research on the complexity of deep inference proofs in classical propositional logic, and also introduce a recent program of research to further develop this subject. Deep inference calculi, due to Guglielmi and others, differ from traditional systems by allowing proof rules to operate on *any* connective occurring in a formula, as opposed to just the main connective. Consequently such calculi are more fine-grained and admit smaller proofs of benchmark classes of tautologies. As well as plainly theoretical motivations, this is advantageous from the point of view of proof communication, allowing for compact and easy-to-check certificates for proofs. I present a graph-based formalism called 'atomic flows', due to Guglielmi and Gundersen following from previous work by Buss, and a rewriting system on them that models proof normalisation while preserving complexity properties. I show how such an abstraction has been influential in work up to now, allowing the obtention of surprisingly strong upper bounds and simulations in analytic deep inference. The biggest open question in the area is the relative complexity between the minimal system KS and a version that allows a form of sharing, KS+. To this end I will consider systems of bounded arithmetic to serve as uniform counterparts to these nonuniform propositional systems. Due to the peculiarities of deep inference calculi, the search for corresponding arithmetic theories takes us into the largely unexplored territories of intuitionistic and substructural arithmetics, requiring novel interplays of tools at the interface of logic and complexity.

ABSTRACT. I discuss recent results enabling expressive process calculi to be embedded in extensions of BV. I also discuss perspectives on understanding the true concurrency of these process embeddings.

ABSTRACT. In this work, we investigate the proof theoretic connections between sequent and nested proof calculi. Specifically, we identify general conditions under which a nested calculus can be transformed into a sequent calculus by restructuring the nested sequent derivation (proof) and shedding extraneous information to obtain a derivation of the same formula in the sequent calculus. These results are formulated generally so that they apply to calculi for intuitionistic, normal and non-normal modal logics.

ABSTRACT. In this talk, we will review the different ways nested sequents have been used to give cut-free deductive systems for various logics, in particular many that cannot be handled in ordinary (Gentzen) calculi, and other applications as interpolation results, realisation theorems for justification logics, etc.

ABSTRACT. We explore the formulation of non-idempotent intersection types for the lambda-calculus in deep-inference using the open-deduction formalism.

ABSTRACT. The reduction of undecidable first-order logic to decidable propositional logic via Herbrand's theorem has long been of interest to theoretical computer science, with the notion of a Herbrand proof motivating the definition of expansion proofs, a compositional formalism that expresses the strictly first-order content of a proof. Recently, a simple deep inference system for first-order logic, KSh2, has been constructed based around the notion of expansion proofs, as a starting point to developing a rich proof theory around this foundation. This abstract summarises the author's recent paper, with a slight change of focus due to the nature of the workshop.