Alessio Guglielmi's Research and Teaching / Deep Inference

Deep InferenceWeb-Based Quantum Bio-Cryptography and Creative Nano-Security for the Cloud

This page tries to be a comprehensive account of the ongoing research on deep inference. Deep inference started as a personal project, but it is now growing fast and I'm struggling to keep pace with all the developments. Some of them I do not understand in detail. Please keep in mind that what I wrote below can be very subjective and not reflect the opinions of the people involved in this research. If you disagree or find inaccuracies, please let me know! If you are an expert of proof theory and want to quickly understand what deep inference is about, go to Deep Inference in One Minute.

News

2016–2019Three-year ANR-FWF project The Fine Structure of Formal Proof Systems and their Computational Interpretations (FISP) at Univ. Paris Diderot/PPS, INRIA Saclay/École Polytechnique, University of Innsbruck, Vienna University of Technology.

14–16 December 2015Workshop on Efficient and Natural Proof Systems in Bath.

3–14 August 2015Two courses on deep inference at ESSLLI 2015.

2013–2016Three-year EPSRC project Efficient and Natural Proof Systems at the University of Bath.

Image credit: Theodor W. Hänsch (Nobel Prize)

1Introduction

[There is a version of this introduction with bibliographic references and examples in the paper Deep Inference.]

Deep inference could succinctly be described as an extreme form of linear logic. It is a methodology for designing proof formalisms that generalise Gentzen formalisms, i.e., the sequent calculus and natural deduction. In a sense, deep inference is obtained by applying some of the main concepts behind linear logic to the formalisms, i.e., to the rules by which proof systems are designed. By doing so, we obtain a better proof theory than the traditional one due to Gentzen. In fact, in deep inference we can provide proof systems for more logics, in a more regular and modular way, with smaller proofs, less syntax, less bureaucracy and we have a chance to make substantial progress towards a solution to the century-old problem of the identity of proofs. The first manuscript on deep inference appeared in 1999 and the first refereed papers in 2001. So far, two formalisms have been designed and developed in deep inference: the calculus of structures and open deduction. A third one, nested sequents, introduces deep inference features into a more traditional Gentzen formalism.

Essentially, deep inference tries to understand proof composition and proof normalisation (in a very liberal sense including cut elimination) in the most logic-agnostic way. Thanks to it we obtain a deeper understanding of the nature of normalisation. It seems that normalisation is a primitive, simple phenomenon that manifests itself in more or less complicated ways that depend more on the choice of representation for proofs rather than their true mathematical nature. By dropping syntactic constraints, as we do in deep inference compared to Gentzen, we get closer to the semantic nature of proof and proof normalisation.

The early inspiration for deep inference came from linear logic. Linear logic, among other ideas, supports the notion that logic has a geometric nature, and that a more perspicuous analysis of proofs is possible if we uncover their geometric shape, hidden behind their syntax. We can give technical meaning to this notion by looking for linearity in proofs. In the computing world, linearity can be interpreted as a way to deal with quantity or resource. The significance of linear logic for computer science has stimulated a remarkable amount of research, that continues to these days, and that ranges from the most theoretical investigations in categorical semantics to the implementation of languages and compilers and the verification of software.

Linear logic expresses locality by relying on Gentzen's formalisms. However, these had been developed for classical mathematical logic, for which linearity is not a primitive, natural notion. While attempting to relate process algebras (which are foundational models of concurrent computation) to linear logic, I realised that Gentzen's formalisms were inherently inadequate to express the most primitive notion of composition in computer science: sequential composition. This is indeed linear, but of a different kind of linearity from that naturally supported by linear logic.

I realised then that the linear logic ideas were to be carried all the way through and that the formalisms themselves had to be `linearised´. Technically, this turned out to be possible by dropping one of the assumptions that Gentzen implicitly used, namely that the (geometric) shape of proofs is directly related to the shape of formulae that they prove. In deep inference, we do not make this assumption, and we get proofs whose shape is much more liberally determined than in Gentzen's formalisms. As an immediate consequence, we were able to capture process-algebras sequential composition, but we soon realised that the new formalism was offering unprecedented opportunities for both a more satisfying general theory of proofs and for more applications in computer science.

1.1Proof Systems

The difference between Gentzen formalisms and deep inference ones is that in deep inference we compose proofs by the same connectives of formulae: if

$\Phi =\begin{array}{c}A\\ ║\\ B\end{array}\phantom{\rule{40px}{0ex}}\mathrm{and}\phantom{\rule{40px}{0ex}}\Psi =\begin{array}{c}C\\ ║\\ D\end{array}$

are two proofs with, respectively, premisses $A$ and $C$ and conclusions $B$ and $D$, then

$\mathrm{\Phi }\wedge \mathrm{\Psi }=\begin{array}{c}A\wedge C\\ ║\\ B\wedge D\end{array}\phantom{\rule{40px}{0ex}}\mathrm{and}\phantom{\rule{40px}{0ex}}\mathrm{\Phi }\vee \mathrm{\Psi }=\begin{array}{c}A\vee C\\ ║\\ B\vee D\end{array}$

are valid proofs with, respectively, premisses $A\wedge C$ and $A\vee C$, and conclusions $B\wedge D$ and $B\vee D$. Significantly, while $\mathrm{\Phi }\wedge \mathrm{\Psi }$ can be represented in Gentzen, $\mathrm{\Phi }\vee \mathrm{\Psi }$ cannot. That is basically the definition of deep inference and it holds for every language, not just propositional classical logic.

As an example, I will show the standard deep inference system for propositional logic. System $\mathrm{SKS}$ is a proof system defined by the following structural inference rules (where $a$ and $\stackrel{-}{a}$ are dual atoms)

$\begin{array}{ccccc}\mathrm{i↓}\frac{t}{a\vee \stackrel{-}{a}}& \phantom{\rule{40px}{0ex}}& \mathrm{w↓}\frac{f}{a}& \phantom{\rule{40px}{0ex}}& \mathrm{c↓}\frac{a\vee a}{a}\\ \mathrm{identity}& & \mathrm{weakening}& & \mathrm{contraction}\\ & & & & \\ \mathrm{i↑}\frac{a\wedge \stackrel{-}{a}}{f}& \phantom{\rule{40px}{0ex}}& \mathrm{w↑}\frac{a}{t}& \phantom{\rule{40px}{0ex}}& \mathrm{c↑}\frac{a}{a\wedge a}\\ \mathrm{cut}& & \mathrm{coweakening}& & \mathrm{cocontraction}\end{array}$

and by the following two logical inference rules:

$\begin{array}{ccc}s\frac{A\wedge \left(B\vee C\right)}{\left(A\wedge B\right)\vee C}& \phantom{\rule{40px}{0ex}}& m\frac{\left(A\wedge B\right)\vee \left(C\wedge D\right)}{\left(A\vee C\right)\wedge \left(B\vee D\right)}\\ \mathrm{switch}& & \mathrm{medial}\end{array}$

A cut-free derivation is a derivation where $\mathrm{i↑}$ is not used, i.e., a derivation in $\mathrm{SKS}\setminus \left\{\mathrm{i↑}\right\}$. In addition to these rules, there is a rule

$=\frac{C}{D}$

such that $C$ and $D$ are opposite sides in one of the following equations:

$\begin{array}{ccccccc}\hfill A\vee B& =& B\vee A\hfill & \phantom{\rule{40px}{0ex}}& \hfill A\vee f& =& A\hfill \\ \hfill A\wedge B& =& B\wedge A\hfill & \phantom{\rule{40px}{0ex}}& \hfill A\wedge t& =& A\hfill \\ \hfill \left(A\vee B\right)\vee C& =& A\vee \left(B\vee C\right)\hfill & \phantom{\rule{40px}{0ex}}& \hfill t\vee t& =& t\hfill \\ \hfill \left(A\wedge B\right)\wedge C& =& A\wedge \left(B\wedge C\right)\hfill & \phantom{\rule{40px}{0ex}}& \hfill f\wedge f& =& f\hfill \end{array}$

We do not always show the instances of rule $=$, and when we do show them, we gather several contiguous instances into one.

For example, this is a valid derivation:

$\begin{array}{c}\left(a\vee b\right)\wedge a\\ ║\\ \left(\left(a\vee b\right)\wedge a\right)\wedge \left(\left(a\vee b\right)\wedge a\right)\end{array}=\begin{array}{|c|}\hline m\frac{\begin{array}{|c|}\hline c\frac{a}{a\wedge a}\\ \hline\end{array}\vee \begin{array}{|c|}\hline c\frac{b}{b\wedge b}\\ \hline\end{array}}{\left(a\vee b\right)\wedge \left(a\vee b\right)}\\ \hline\end{array}\wedge \begin{array}{|c|}\hline c\frac{a}{a\wedge a}\\ \hline\end{array}$

This derivation illustrates a general principle in deep inference: structural rules on generic formulae (in this case a cocontraction) can be replaced by corresponding structural rules on atoms (in this case $\mathrm{c↑}$).

It is interesting to note that the inference rules for classical logic, as well as the great majority of rules for any logic, all derive from a common template which has been distilled from the semantics of a purely linear logic in the first deep inference paper. Since this phenomenon is very surprising, especially for structural rules such as weakening and contraction, we believe that we might be dealing with a rather deep aspect of logic and we are currently investigating it.

1.2Proof-Theoretical Properties

Locality and linearity are foundational concepts for deep inference, in the same spirit as they are for linear logic. Going for locality and linearity basically means going for \emph{complexity bounded by a constant}. This last idea introduces geometry into the picture, because bounded complexity leads us to equivalence modulo continuous deformation. In a few words, the simple and natural definition of deep inference that we have seen above captures these ideas about linearity, locality and geometry, and can consequently be exploited in many ways, and notably:

• to recover a De Morgan premiss-conclusion symmetry that is lost in Gentzen;
• to obtain new notions of normalisation in addition to cut elimination;
• to shorten analytic proofs by exponential factors compared to Gentzen;
• to obtain quasipolynomial-time normalisation for propositional logic;
• to express logics that cannot be expressed in Gentzen;
• to make the proof theory of a vast range of logics regular and modular;
• to get proof systems whose inference rules are local, which is usually impossible in Gentzen;
• to inspire a new generation of proof nets and semantics of proofs;
• to investigate the nature of cut elimination;
• to type optimised versions of the λ-calculus that are not typeable in Gentzen;
• to model process algebras;
• to model quantum causal evolution ...
• ... and much more.

One of the open questions is whether deep inference might have a positive influence on the proof-search-as-computation paradigm and possibly on focusing. This subject has been so far almost unexplored, but some preliminary work looks very promising.

The core topic of every proof-theoretic investigation, namely normalisation, deserves a special mention. Traditionally, normalisation is at the core of proof theory, and this is of course the same for deep inference. Normalisation in deep inference is not much different, in principle, from normalisation in Gentzen theory. In practice, however, the more liberal proof composition mechanism of deep inference completely invalidates the techniques (and the intuition) behind cut elimination procedures in Gentzen systems. Much of the effort of these 15 years of research on deep inference went into recovering a normalisation theory. One of the main ideas is called splitting, and at present itis the most general method we know for eliminating cuts in deep inference.

On the other hand, we now have techniques that are not as widely applicable but that are of a completely different nature from splitting, which is combinatorial. A surprising, relatively recent result consists in exploiting deep inference's locality to obtain the first purely geometric normalisation procedure, by a topological device that we call atomic flows. This means that, at least for classical logic and logics that extend it, cut elimination can be understood as a process that is completely independent from logical information: only the shape of the proof, determined by its structural information (creation, duplication and erasing of atoms) matters. Logical information, such as the connectives in formulae, do not matter. This hints at a deeper nature of normalisation than what we thought so far. It seems that normalisation is a primitive, simple phenomenon that manifests itself in more or less complicated ways that depend more on the choice of representation for proofs rather than their true mathematical nature.

1.3History

Deep inference comes from linear logic and process algebras; more specifically, it comes from seeing proofs as concurrent processes. The first development has been the definition of the calculus of structures and a cut elimination proof for the logic BV, which was studied for being the logical counterpart of the core of the process algebra CCS. We realised that the techniques developed for BV had a much wider applicability, so we broadly developed the calculus of structures and studied its many novel normalisation properties. The initial phase of development took place in Dresden, from 1999 to 2003; now deep inference is developed in several laboratories around the world. The recent results on modal and intuitionistic logics, proof nets and semantics, and implementations, complete the establishing of deep inference as a solid and comprehensive methodology in proof theory.

2Papers

The following material is broad in scope; if you are new to deep inference and the calculus of structures, start here:

Abstracts ON or OFF (Javascript required).

• Deep Inference
Alessio Guglielmi
Pdf30 November 2014
All About Proofs, Proofs for All, Mathematical Logic and Foundations, College Publications, pp. 164–172, 2015

• Nested Deduction in Logical Foundations for Computation
Nicolas Guenot
Abstract
Pdf10 April 2013
PhD thesis, defended on 10 April 2013

• Towards a Theory of Proofs of Classical Logic
Lutz Straßburger
Pdf3 December 2010
Habilitation thesis

• A General View of Normalisation Through Atomic Flows
Tom Gundersen
Abstract
Pdf12 August 2010
PhD thesis, defended on 10 November 2009

• Nested Sequents
Kai Brünnler
Abstract
Pdf13 April 2010
Habilitation thesis

Ozan Kahramanoğulları
Abstract
Pdf11 September 2006
PhD thesis, defended on 21 December 2006

• Categorical Models of First Order Classical Proofs
Richard McKinley
Abstract
Pdf30 March 2006
PhD thesis, defended on 17.3.2006

• Deep Inference and Its Normal Form of Derivations
Kai Brünnler
Abstract
Pdf29 March 2006
CiE 2006, LNCS 3988, pp. 65–74

• Deep Inference and Symmetry in Classical Proofs
Kai Brünnler
Abstract
PdfFebruary 2004
You can buy this book at Logos-Verlag and at Amazon

• Linear Logic and Noncommutativity in the Calculus of Structures
Lutz Straßburger
Abstract
PdfPdf in booklet format25 July 2003
PhD thesis, defended on 24 July 2003

In the rest of the section, all the papers I know of are listed according to their subject, in no particular order.

2.1Classical and Intuitionistic Logic

So far, for classical logic in the calculus of structures we achieved:

• the cut rule trivially reduces to atomic form;
• one can show cut elimination for the propositional fragment by the simplest cut elimination argument to date;
• the propositional fragment is fully local, including contraction;
• first order classical logic can be entirely made finitary;
• cut elimination and decomposition theorems are proved;
• a typed lambda-calculus with explicit sharing can be obtained via a Curry-Howard interpretation of deep inference.

We can present intuitionistic logic in the calculus of structures with a fully local, cut-free system. The logic of bunched implications BI can be presented in the calculus of structures. Japaridze's cirquent calculus benefits from a deep-inference presentation, in particular in the case of propositional logic.

The following papers exist, in addition to Deep Inference and Its Normal Form of Derivations and Deep Inference and Symmetry in Classical Proofs, mentioned above:

Abstracts ON or OFF (Javascript required).

• No Complete Linear Term Rewriting System for Propositional Logic
Anupam Das and Lutz Straßburger
Abstract
Pdf14 February 2015
Accepted at RTA 2015, LIPIcs

• Symmetric Normalisation for Intuitionistic Logic
Nicolas Guenot and Lutz Straßburger
Abstract
Pdf20 May 2014
CSL-LICS 2014, pp. 45:1–10

• A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus
Tom Gundersen, Willem Heijltjes and Michel Parigot
Abstract
Pdf10 October 2013
LPAR-19, LNCS 8312, pp. 340–354

• Atomic Lambda Calculus: A Typed Lambda-Calculus with Explicit Sharing
Tom Gundersen, Willem Heijltjes and Michel Parigot
Abstract
Pdf21 May 2013
LICS 2013 Proceedings (IEEE), pp. 311–320

• Nested Proof Search as Reduction in the λ-calculus
Nicolas Guenot
Abstract
Pdf12 May 2011
PPDP 2011, ACM, pp. 183–193

• Breaking Paths in Atomic Flows for Classical Logic
Alessio Guglielmi, Tom Gundersen and Lutz Straßburger
Abstract
Pdf29 April 2010
LICS 2010 Proceedings (IEEE), pp. 284–293

• An Algorithmic Interpretation of a Deep Inference System
Kai Brünnler and Richard McKinley
Abstract
Pdf22 September 2008
LPAR 08, LNCS 5330, pp. 482–496

• Cirquent Calculus Deepened
Giorgi Japaridze
Abstract
Pdf1 April 2008
Journal of Logic and Computation, 18 (6) 2008, pp. 983–1028

• Normalisation Control in Deep Inference Via Atomic Flows
Alessio Guglielmi and Tom Gundersen
Abstract
Journal page (pdf/postscript)31 March 2008
Logical Methods in Computer Science 4 (1:9) 2008, pp. 1–36

• The Logic of Bunched Implications: A Memoir
Benjamin Robert Horsfall
Abstract
PdfJune 2007
MSc thesis, successfully defended in August 2007

• A Characterisation of Medial as Rewriting Rule
Lutz Straßburger
Abstract
Pdf13 April 2007
RTA 2007, LNCS 4533, pp. 344–358

• A Local System for Intuitionistic Logic
Alwen Tiu
Abstract

• Locality for Classical Logic
Kai Brünnler
Abstract
Pdf10 March 2006
Notre Dame Journal of Formal Logic 47 (4), pp. 557–580, 2006
Review by Sara Negri
Note about the review: All the concerns of the reviewer are addressed in the paper Two Restrictions on Contraction (which is among the references of the reviewed paper).

• Cut Elimination Inside a Deep Inference System for Classical Predicate Logic
Kai Brünnler
Abstract
Pdf9 March 2005
Studia Logica 82 (1), pp. 51–71, 2006

• A First Order System with Finite Choice of Premises
Kai Brünnler and Alessio Guglielmi
Abstract
Pdf1 December 2003
Presented at First Order Logic 75 under the title A Finitary System for First Order Logic; appeared in Hendricks et al., editor, First-Order Logic Revisited, Logos Verlag, Berlin, 2004, pp. 59–74

• Two Restrictions on Contraction
Kai Brünnler
Abstract
Pdf24 November 2003
Logic Journal of the Interest Group in Pure and Applied Logics 11 (5), pp. 525–529

• Consistency Without Cut Elimination
Kai Brünnler and Alessio Guglielmi
Abstract
Pdf10 September 2003It is contained in A First Order System with Finite Choice of Premises

• Atomic Cut Elimination for Classical Logic
Kai Brünnler
Abstract
Pdf10 April 2003
CSL 2003, LNCS 2803, pp. 86–97

• A Local System for Classical Logic
Kai Brünnler and Alwen Fernanto Tiu
Abstract
Pdf2 October 2001Now replaced by Locality for Classical Logic
LPAR 2001, LNCS 2250, pp. 347–361

2.2Proof Complexity

The basic proof complexity properties of propositional logic in the calculus of structures are known. Deep inference is as powerful as Frege systems, and more powerful than Gentzen systems, in the restriction to analytic systems.

The following papers exist:

Abstracts ON or OFF (Javascript required).

• On the Power of Substitution in the Calculus of Structures
Novak Novaković and Lutz Straßburger
Abstract
Pdf7 April 2015
ACM Transactions on Computational Logic 16 (3:19) 2015, pp. 1–20

• On the Relative Proof Complexity of Deep Inference Via Atomic Flows
Anupam Das
Abstract

• On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems
Anupam Das
Abstract
PdfExtended version PDF16 May 2014
CSL-LICS 2014, pp. 36:1–10

• Quasipolynomial Normalisation in Deep Inference Via Atomic Flows and Threshold Formulae
Paola Bruscoli, Alessio Guglielmi, Tom Gundersen and Michel Parigot
Abstract

• Rewriting with Linear Inferences in Propositional Logic
Anupam Das
Abstract
Pdf15 February 2013
RTA 2013, LIPIcs 21, pp. 158–173

• Extension without Cut
Lutz Straßburger
Abstract
Pdf31 July 2012
Annals of Pure and Applied Logic 163(12) 2012, pp. 1995–2007

• On the Proof Complexity of Cut-Free Bounded Deep Inference
Anupam Das
Abstract
Pdf25 April 2011
Tableaux 2011, LNCS 6793, pp. 134–148

• On the Proof Complexity of Deep Inference
Paola Bruscoli and Alessio Guglielmi
Abstract
Pdf19 April 2009
ACM Transactions on Computational Logic 10 (2:14) 2009, pp. 1–34

• Proof complexity of the Cut-Free Calculus of Structures
Emil Jeřábek
Abstract
Pdf30 April 2008
Journal of Logic and Computation 19 (2) 2009, pp. 323–339, 2009

2.3Nested Sequents

A new formalism called 'nested sequents' has been defined, which is especially suitable to modal logics.

The following papers exist, in addition to Nested Sequents, mentioned above:

Abstracts ON or OFF (Javascript required).

• Label-free Modular Systems for Classical and Intuitionistic Modal Logics
Sonia Marin and Lutz Straßburger
Abstract
Pdf6 June 2014
Advances in Modal Logic 2014, pp. 387–406

• Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic
Ranald Clouston, Jeremy Dawson, Rajeev Goré and Alwen Tiu
Abstract
Pdf8 July 2013
CSL 2013, LIPIcs 23, pp. 197–214

• Nested Sequent Calculi for Normal Conditional Logics
Régis Alenda, Nicola Olivetti and Gian Luca Pozzato
Abstract
Pdf1 June 2013
To appear on Journal of Logic and Computation

• Algebra, Proof Theory and Applications for an Intuitionistic Logic of Propositions, Actions and Adjoint Modal Operators
Abstract
Pdf31 May 2013
ACM Transactions on Computational Logic 14 (4:34) 2013, pp. 1–37

• Cut Elimination in Nested Sequents for Intuitionistic Modal Logics
Lutz Straßburger
Abstract
Pdf7 January 2013
FoSSaCS 2013, LNCS 7794, pp. 209–224

• Labelled Tree sequents, Tree Hypersequents and Nested (Deep) Sequents
Rajeev Goré and Revantha Ramanayake
Abstract
Pdf5 October 2012
Advances in Modal Logic 2012, pp. 279–299

• Nested Sequent Calculi for Conditional Logics
Régis Alenda, Nicola Olivetti and Gian Luca Pozzato
Abstract
Pdf16 July 2012
JELIA 2012, LNCS 7519, pp. 14–27

• Nested Sequents for Intuitionistic Logics
Melvin Fitting
Abstract
Pdf8 July 2012
Notre Dame Journal of Formal Logic 55 (1), pp. 41–61, 2014

• Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures
Alwen Tiu and Egor Ianovski and Rajeev Goré
Abstract
Pdf15 June 2012
Advances in Modal Logic 2012, pp. 516–537

• Syntactic Cut-Elimination for a Fragment of the Modal Mu-Calculus
Kai Brünnler and Thomas Studer
Abstract
Pdf14 May 2012
Annals of Pure and Applied Logic 163(12), pp. 1838–1853, 2012

• Proving Completeness for Nested Sequent Calculi
Melvin Fitting
Abstract
Pdf4 October 2011
Logic without Frontiers, College Publications, pp. 145–154, 2011

• Prefixed Tableaus and Nested Sequents
Melvin Fitting
Abstract
Pdf14 September 2011
Annals of Pure and Applied Logic 163(3), pp. 291–313, 2012

• On the Correspondence Between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
Rajeev Goré, Linda Postniece and Alwen Tiu
Abstract

• Proof Theory and Proof Search of Bi-Intuitionistic and Tense Logic
Linda Postniece
Abstract
Pdf21 November 2010
PhD thesis, defended on March 2011

• How to Universally Close the Existential Rule
Kai Brünnler
Abstract
Pdf (long version)31 July 2010
LPAR-17, LNCS 6397, pp. 172–186

• Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic
Rajeev Goré, Linda Postniece and Alwen Tiu
Abstract
Pdf29 June 2010
Advances in Modal Logic 2010, pp 156–177

• A Syntactic Realization Theorem for Justification Logics
Kai Brünnler, Remo Goetschi and Roman Kuznets
Abstract
Pdf3 April 2010
Advances in Modal Logic 2010, pp 39–58

• A Note on Uniform Interpolation Proofs in Modal Deep Inference Calculi
Marta Bílková
Abstract
21 September 2009
TbiLLC 2009, LNAI 6618, pp. 30–45

• Deep Inference in Bi-intuitionistic Logic
Linda Postniece
Abstract
Pdf7 June 2009
WoLLIC 2009, LNCS 5514, pp. 320–334

• Modular Sequent Systems for Modal Logic
Kai Brünnler and Lutz Straßburger
Abstract
Pdf23 April 2009
Tableaux 2009, LNCS 5607, pp. 152–166
Attention, this paper contains some serious mistakes. The authors are working on a corrected version.

• Syntactic Cut-Elimination for Common Knowledge
Kai Brünnler and Thomas Studer
Abstract

• Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents
Rajeev Goré, Linda Postniece and Alwen Tiu
Abstract
Pdf15 September 2008
Advances in Modal Logic 2008, pp 43–66

• Deep Sequent Systems for Modal Logic
Kai Brünnler
Abstract

2.4Modal Logic

We can present systematically several normal propositional modal logics, including S5, B and K5, for which cut elimination is proved. We also investigated geometric theories, some of which we expressed in the calculus of structures.

The following papers exist:

Abstracts ON or OFF (Javascript required).

• Deep Inference for Hybrid Logic
Lutz Straßburger
Abstract
Pdf15 May 2007
Proceedings of International Workshop on Hybrid Logic 2007 (HyLo 2007), pp. 13–22

• Classical Modal Display Logic in the Calculus of Structures and Minimal and Cut-free Deep Inference Calculi for S5
Rajeev Goré and Alwen Tiu
Abstract
Pdf4 May 2007
Journal of Logic and Computation 17 (4) 2007, pp. 767–794

• A Deep Inference System for the Modal Logic S5
Phiniki Stouppa
Abstract
Pdf1 March 2006
Studia Logica 85 (2) 2007, pp. 199–214

• Purity Through Unravelling
Robert Hein and Charles Stewart
Abstract
Pdf25 June 2005
Proceedings of Structures and Deduction '05, pp. 126–143

• Geometric Theories and Modal Logic in the Calculus of Structures
Robert Hein
Abstract
Gzipped postscript20 March 2005
MSc thesis, successfully defended on 23 March 2005

• The Design of Modal Proof Theories: The Case of S5
Phiniki Stouppa
Abstract
Pdf20 October 2004
MSc thesis, successfully defended on 27 October 2004

• A Systematic Proof Theory for Several Modal Logics
Charles Stewart and Phiniki Stouppa
Abstract
Postscript2 September 2004
Advances in Modal Logic 2004, pp. 309–333

2.5Linear Logic

Linear logic enjoys presentations in deep inference that obtain the expected properties of locality, with rather astounding decomposition theorems and the usual, general normalisation results.

The following papers exist, in addition to Linear Logic and Noncommutativity in the Calculus of Structures, mentioned above:

Abstracts ON or OFF (Javascript required).

• Equality and Fixpoints in the Calculus of Structures
Kaustuv Chaudhuri and Nicolas Guenot
Abstract
Pdf2 June 2014
CSL-LICS 2014, pp. 30:1–10

• Interaction and Depth Against Nondeterminism in Proof Search
Ozan Kahramanoğulları
Abstract
Pdf29 May 2014
Logical Methods in Computer Science 10 (2:5) 2014, pp. 1–49
Interana: interactive multiplicative linear logic prover

• The Focused Calculus of Structures
Kaustuv Chaudhuri, Nicolas Guenot and Lutz Straßburger
Abstract
Pdf25 August 2011
CSL 2011, LIPIcs 12, pp. 159–173

• Focused Proof Search for Linear Logic in the Calculus of Structures
Nicolas Guenot
Abstract
Pdf23 June 2010
ICLP 2010, technical communication, LIPIcs 7, pp. 84–93

• Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
Lutz Straßburger
Abstract
Pdf10 April 2009
TLCA 2009, LNCS 5608, pp. 309–324
Pdf with proofs in appendix

• MELL in the Calculus of Structures
Lutz Straßburger
Abstract
Pdf24 November 2003
Theoretical Computer Science 309, pp. 213–285

• A Local System for Linear Logic
Lutz Straßburger
Abstract

2.6Commutative/Non-commutative Linear Logic

We conservatively extend mixed multiplicative and multiplicative exponential linear logic with a self-dual non-commutative operator. The systems so obtained cannot be presented in the sequent calculus, but they enjoy the usual properties of locality, decomposition and cut elimination available in the calculus of structures. We can present Yetter's cyclic linear logic in the calculus of structures and prove cut elimination; interestingly, cyclicity is naturally subsumed by deep inference. New, purely proof-theoretical, techniques are developed for reducing the non-determinism in the calculus of structures.

The following papers exist, in addition to Linear Logic and Noncommutativity in the Calculus of Structures, mentioned above:

Abstracts ON or OFF (Javascript required).

• A Deep Inference System with a Self-Dual Binder Which Is Complete for Linear Lambda Calculus
Luca Roversi
Abstract
Pdf25 January 2014
To appear on Journal of Logic and Computation

• A Logical Basis for Quantum Evolution and Entanglement
Richard F. Blute, Alessio Guglielmi, Ivan T. Ivanov, Prakash Panangaden and Lutz Straßburger
Abstract
Pdf18 July 2013
In Categories and Types in Logic, Language, and Physics, LNCS 8222, pp. 90–107

• Communication, and Concurrency with Logic-Based Restriction Inside a Calculus of Structures
Luca Roversi
Abstract
Pdf19 December 2012
Submitted

• Linear Lambda Calculus and Deep Inference
Luca Roversi
Abstract

• A System of Interaction and Structure V: The Exponentials and Splitting
Alessio Guglielmi and Lutz Straßburger
Abstract
Pdf21 September 2010
Mathematical Structures in Computer Science, 21 (3) 2011, pp. 563–584
This paper is the second part resulted from splitting into two parts the paper A System of Interaction and Structure IV: The Exponentials (which was previously titled A Non-commutative Extension of Multiplicative Exponential Linear Logic and was the journal version of A Non-commutative Extension of MELL).

• A System of Interaction and Structure IV: The Exponentials and Decomposition
Lutz Straßburger and Alessio Guglielmi
Abstract
Pdf27 July 2010
ACM Transactions on Computational Logic 12 (4:23) 2011, pp. 1–39
This paper is the first part resulted from splitting into two parts the paper A System of Interaction and Structure IV: The Exponentials (which was previously titled A Non-commutative Extension of Multiplicative Exponential Linear Logic and was the journal version of A Non-commutative Extension of MELL).

• Deep Inference and Probabilistic Coherence Spaces
Richard Blute, Prakash Panangaden and Sergey Slavnov
Abstract
Pdf10 February 2009
Applied Categorical Structures 20 2012, pp. 209–228

• System BV Is NP-Complete
Ozan Kahramanoğulları
Abstract

• A System of Interaction and Structure
Alessio Guglielmi
Abstract
Pdf27 January 2007
ACM Transactions on Computational Logic 8 (1:1) 2007, pp. 1–64
The journal version has been butchered by the editorial process, but the preprint (linked here) is fine.
At the end of 2012, this was the most cited article appeared in ACM TOCL in the previous five years.

• Reducing Nondeterminism in the Calculus of Structures
Ozan Kahramanoğulları
Abstract
Pdf23 August 2006
LPAR 2006, LNCS 4246, pp. 272–286

• A System of Interaction and Structure II: The Need for Deep Inference
Alwen Tiu
Abstract
Pdf3 April 2006
Logical Methods in Computer Science 2 (2:4) 2006, pp. 1–24
There are pictures that help understanding this paper in Alwen Tiu's MSc thesis Properties of a Logical System in the Calculus of Structures

• Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity
Pietro Di Gianantonio
Abstract
Pdf15 April 2004
CSL 2004, LNCS 3210, pp. 130–144

• A Non-commutative Extension of MELL
Alessio Guglielmi and Lutz Straßburger
Abstract
Pdf9 August 2002
LPAR 2002, LNCS 2514, pp. 231–246

• The Undecidability of System NEL
Lutz Straßburger
Abstract

• A1-Unification
Alwen Fernanto Tiu
Gzipped postscript19 February 2002
Technical Report WV-01-08, Technische Universität Dresden

• Combining A1- and AC1-Unification Sharing Unit
Alwen Fernanto Tiu
Gzipped postscript19 February 2002
Technical Report WV-01-09, Technische Universität Dresden

• Properties of a Logical System in the Calculus of Structures
Alwen Fernanto Tiu
Abstract
Pdf12 September 2001Now replaced by A System of Interaction and Structure II: The Need for Deep-Inference
MSc thesis, successfully defended on 1 August 2001, Technical Report WV-01-06, Technische Universität Dresden

• Non-commutativity and MELL in the Calculus of Structures
Alessio Guglielmi and Lutz Straßburger
Abstract
Pdf28 June 2001
CSL 2001, LNCS 2142, pp. 54–68

• A Calculus of Order and Interaction
Alessio Guglielmi
This paper has been thoroughly rewritten as A System of Interaction and Structure. The introduction of the new paper has not been written under the effect of psychotropic substances. Please forget about this paper.
Technical Report WV-99-04, Technische Universität Dresden

2.7Proof Nets, Semantics of Proofs and the War to Bureaucracy

Deep inference and the calculus of structures are influencing the design of a new generation of proof nets. Moreover, they offer new insight for semantics of proofs and categorical proof theory. Finally, they open decisive new perspectives in the fight against bureaucracy.

The following papers exist, in addition to A General View of Normalisation Through Atomic Flows and Categorical Models of First Order Classical Proofs, mentioned above:

Abstracts ON or OFF (Javascript required).

• The Structure of Interaction
Stéphane Gimenez and Georg Moser
Abstract
Pdf4 July 2013
CSL 2013, LIPIcs 23, pp. 316–331

• A Proof Calculus Which Reduces Syntactic Bureaucracy
Alessio Guglielmi, Tom Gundersen and Michel Parigot
Abstract
Pdf12 April 2010
RTA 2010, Leibniz International Proceedings in Informatics (LIPIcs) 6, pp. 135–150
This paper supersedes the note Formalism A.

• What Is the Problem with Proof Nets for Classical Logic?
Lutz Straßburger
Abstract
Pdf6 April 2010
CiE 2010, LNCS 6158, pp. 406–416

• From Deep Inference to Proof Nets Via Cut Elimination
Lutz Straßburger
Abstract

• On the Axiomatisation of Boolean Categories with and without Medial
Lutz Straßburger
Abstract

• What Is a Logic, and What Is a Proof?
Lutz Straßburger
Abstract
Pdf23 October 2006
Logica Universalis—Towards a General Theory of Logic, pp. 135–152, Birkhäuser, 2007

• Proof Nets and the Identity of Proofs
Lutz Straßburger
Abstract
Pdf20 October 2006
Technical Report 6013, INRIA

• From Proof Nets to the Free *-Autonomous Category
François Lamarche and Lutz Straßburger
Abstract
Pdf5 October 2006Journal version of On Proof Nets for Multiplicative Linear Logic with Units
Logical Methods in Computer Science 2 (4:3) 2006, pp. 1–44

• Completeness of MLL Proof-Nets w.r.t. Weak Distributivity
Jean-Baptiste Joinet
Abstract
Pdf8 September 2006
The Journal of Symbolic Logic 72 (1) 2007, pp. 159–170
Invited talk at WoLLIC 2003, under the title 'Calculus of Structures and Proof Nets', Electronic Notes in Theoretical Computer Science 84; a short version appeared in the proceedings of Structures and Deduction '05, pp. 81–94

• Exploring the Gap between Linear and Classical Logic
François Lamarche
Abstract
Pdf27 June 2006
Theory and Applications of Categories 18 (17) 2007, pp. 473–535

• The Three Dimensions of Proofs
Yves Guiraud
Abstract

• On Two Forms of Bureaucracy in Derivations
Kai Brünnler and Stéphane Lengrand
Abstract
Pdf10 June 2005
Proceedings of Structures and Deduction '05, pp. 69–80
This is further expanded in Ch. 11 of Stéphane Lengrand's PhD thesis Normalisation & Equivalence in Proof Theory & Type Theory (2007 Ackermann Award of the EACSL)

• Constructing Free Boolean Categories
François Lamarche and Lutz Straßburger
Abstract

• Classical Categories and Deep Inference
Richard McKinley
Abstract
Pdf31 March 2005
Proceedings of Structures and Deduction '05, pp. 19–33

• Naming Proofs in Classical Propositional Logic
François Lamarche and Lutz Straßburger
Abstract
Pdf31 January 2005
TLCA 2005, LNCS 3461, pp. 246–261

• Deep Inference Proof Theory Equals Categorical Proof Theory Minus Coherence
Dominic Hughes
Abstract
Pdf6 October 2004

• On Proof Nets for Multiplicative Linear Logic with Units
Lutz Straßburger and François Lamarche
Abstract
Pdf30 June 2004
CSL 2004, LNCS 3210, pp. 145–159

2.8Language Design

Thanks to a self-dual non-commutative extension of linear logic one gets the first purely logical account of sequentiality in proof search. The new logical operators make possible a new approach to partial order planning and its relation to concurrency.

Abstracts ON or OFF (Javascript required).

• On Linear Logic Planning and Concurrency
Ozan Kahramanoğulları
Abstract

• A Deductive Compositional Approach to Petri Nets for Systems Biology
Ozan Kahramanoğulları
Abstract
Pdf18 September 2007
Presented as poster at CMSB '07

• Labeled Event Structure Semantics of Linear Logic Planning
Ozan Kahramanoğulları
Pdf17 January 2005
Presented at 1st World Congress on Universal Logic

• Towards Planning as Concurrency
Ozan Kahramanoğulları
Abstract
Pdf19 October 2004
Artificial Intelligence and Applications 2005, ACTA Press, pp. 197–202

• A Purely Logical Account of Sequentiality in Proof Search
Paola Bruscoli
Abstract
Pdf12 August 2002
ICLP 2002, LNCS 2401, pp. 302–316

2.9Implementations

Ozan Kahramanoğulları, Pierre-Etienne Moreau and Antoine Reilles are implementing calculus-of-structures proof systems in Maude and in Tom. Ozan managed to achieve efficiency without sacrificing proof theoretic cleanliness, and he is obtaining results of independent theoretical interest. There are two slides presentations:

Max Schäfer has built a graphical proof editor in Java, called GraPE, for the Maude modules written by Ozan Kahramanoğulları; this means that one can interactively build and find proofs in several deep-inference systems.

Abstracts ON or OFF (Javascript required).

• Ingredients of a Deep Inference Theorem Prover
Ozan Kahramanoğulları
Abstract
Pdf24 June 2008
Short paper at CL&C'08

• Maude as a Platform for Designing and Implementing Deep Inference Systems
Ozan Kahramanoğulları
Abstract
Pdf16 September 2007
RULE '07, Electronic Notes in Theoretical Computer Science 219, 2008, pp. 35–50

• Canonical Abstract Syntax Trees
Antoine Reilles
Abstract
Pdf28 March 2006
Proceedings of 6th International Workshop on Rewriting Logic and Its Applications, Electronic Notes in Theoretical Computer Science 176, 2007, pp. 165–179

• Implementing Deep Inference in TOM
Ozan Kahramanoğulları, Pierre-Etienne Moreau, Antoine Reilles
Abstract
Pdf23 April 2005
Proceedings of Structures and Deduction '05, pp. 158–172

• System BV Without the Equalities for Unit
Ozan Kahramanoğulları
Abstract
Pdf4 August 2004
ISCIS 2004, LNCS 3280, pp. 986–995

• From the Calculus of Structures to Term Rewriting Systems
Steffen Hölldobler and Ozan Kahramanoğulları
Abstract
13 June 2004
Technical Report WV-04-03, Technische Universität Dresden

• Implementing System BV of the Calculus of Structures in Maude
Ozan Kahramanoğulları
Abstract
Pdf13 June 2004
Proceedings of ESSLLI 2004-Student Session

3Counterexamples

Finding counterexamples is very important to us. Counterexamples are typically of a very combinatorial nature, due to the new combinatorial possibilities offered by deep inference.

4Notes

• Confluent and Natural Cut Elimination in Classical LogicAlessio Guglielmi and Benjamin RalphWe show that, in deep inference, there is a natural and confluent cut elimination procedure that has a strikingly simple semantic justification. We proceed in two phases: we first tackle the propositional case with a construction that we call the 'experiments method'. Here we build a proof made of as many derivations as there are models of the given tautology. Then we lift the experiment method to the predicate calculus, by tracing all the existential witnesses, and in so doing we reconstruct the Herbrand theorem. The confluence of the procedure is essentially taken care of by the commutativity and associativity of disjunction.31 March 2015Accepted at Proof, Computation, Complexity 2015

• Subatomic Proof SystemsAndrea Aler Tubella and Alessio GuglielmiWe show a proof system that generates propositional proofs by employing a single, linear, simple and regular inference rule scheme. The main idea is to consider atoms as self-dual, noncommutative binary logical relations and build formulae by freely composing units by atoms, disjunction and conjunction. If we restrict proofs to formulae where no atom occurs in the scope of another atom, we fully and faithfully recover a deduction system for propositional logics in the usual sense, where traditional proof analysis and transformation techniques such as cut elimination can be studied.30 March 2015Accepted at Proof, Computation, Complexity 2015

• A Subatomic Proof SystemAndrea Aler Tubella and Alessio GuglielmiIn this work we show a proof system, called SA, that generates propositional proofs by employing a single, linear, simple and regular inference rule scheme. The main idea is to consider atoms as self-dual, noncommutative binary logical relations and build formulae by freely composing units by atoms, disjunction and conjunction. If we restrict proofs to formulae where no atom occurs in the scope of another atom, we fully and faithfully recover a deduction system for propositional logic in the usual sense, where traditional proof analysis and transformation techniques such as cut elimination can be studied.5 July 2014

• The Commutative/Noncommutative Linear Logic BVAlessio GuglielmiThis brief survey contains an informal presentation of the commutative/noncommutative linear logic BV in terms of a naif space-temporal model. BV improves on the ability of linear logic to model spatial structure by satisfactorily capturing temporal structure in programming languages and quantum physics. I provide a guide to the literature on BV and suggest that the only satisfactory treatment for it can be obtained in the proof-theoretic methodology of deep inference.8 May 2014

• The Logic BV and Quantum CausalityRichard Blute, Prakash Panangaden and Lutz StraßburgerWe describe how a logic with commutative and noncommutative connectives can be used for capturing the essence of discrete quantum causal propagation.12 September 2008Superseded by A Logical Basis for Quantum Evolution and Entanglement

• Polynomial Size Deep-Inference Proofs Instead of Exponential Size Shallow-Inference ProofsAlessio GuglielmiBy a simple example, I show how deep inference can provide for an exponential speed-up in the size of proofs with respect to shallow inference.22 September 2007SlidesSuperseded by On the Proof Complexity of Deep Inference

• Finitary CutAlessio GuglielmiWe all know that the traditional cut rule is considered infinitary. But if we reduce the cut rule to atomic form, as we always can do in the calculus of structures, is atomic cut still infinitary? Not really.22 September 2007Superseded by A First Order System with Finite Choice of Premises

• On Analytic Inference Rules in the Calculus of StructuresPaola Bruscoli and Alessio GuglielmiWe discuss the notion of analytic inference rule for propositional logics in the calculus of structures.25 November 2009

• Interaction and Depth Against Nondeterminism in Proof SearchOzan KahramanoğullarıWe argue that, by exploiting an interaction and depth scheme in the logical expressions, the nondeterminism in proof search can be reduced without losing the shorter proofs and breaking proof theoretical properties.23 April 2007Presented at Automated Reasoning Workshop 2007

• ButterfliesAlessio GuglielmiIf you're interested in NEL and BV, try and find the mistake in this note.29 July 2005

• Some News on Subatomic LogicAlessio GuglielmiI found a simple explanation for the soundness of the subatomic inference rule.28 July 2005

• Red and BlueAlessio GuglielmiThe sequent calculus is often colour blind, but not always; the calculus of structures has a consistent behaviour.26 July 2005

• The Problem of Bureaucracy and Identity of Proofs from the Perspective of Deep InferenceAlessio GuglielmiSome discussion and then the first attempt at wired/weird deduction.17 June 2005Proceedings of Structures and Deduction '05, pp. 53–68

• Getting Formalisms A and B by Proof-Terms and Typing SystemsStéphane Lengrand and Kai Brünnler 11 February 2005Expanded into On Two Forms of Bureaucracy in Derivations

• Formalism BAlessio GuglielmiInference rules operate on derivations.20 December 2004

• Using BV to Describe Causal Quantum EvolutionPrakash PanangadenIn this note I describe how to capture the kinematics of quantum causal evolution using a logic called BV developed by the Calculus of Structures group at Dresden.5 July 2004

• Formalism AAlessio GuglielmiI generalise the notion of derivation for taking care of a certain kind of bureaucracy.23 April 2004Superseded by A Proof Calculus Which Reduces Syntactic Bureaucracy

• Resolution in the Calculus of StructuresAlessio GuglielmiIt is possible to search for cut-free proofs by the resolution strategy in the calculus of structures; the sequent calculus does not allow the same freedom.29 September 2003

• MismatchAlessio GuglielmiThere is a mismatch between meta and object levels in many calculi, like the sequent calculus and natural deduction. The mismatch has undesirable proof theoretical consequences, the most important being the inability to design deductive systems.24 August 2003Brief note for the specialist, posted to the Foundations of Mathematics and Proof Theory lists

• Normalisation Without Cut EliminationAlessio GuglielmiI propose a possible notion of equivalence for proofs in classical logic, sort of a normal form for case analysis.25 February 2003

• Subatomic LogicAlessio GuglielmiOne can unify classical and linear logic by using only two simple, linear, 'hyper' inference rules; they generate nice systems for all the fragments, where all rules are local. The various logics are determined by the algebra of their units, for example boolean algebra determines classical logic. We can prove cut elimination easily and once and for all in the two-rule system, and the procedure scales down to all the derived fragments.21 November 2002

• On Lafont's CounterexampleAlessio GuglielmiLafont's counterexample shows why cut elimination in the sequent calculus of classical logic is not confluent. I show here that the counterexample doesn't work in the calculus of structures.1 November 2002

• RecipeAlessio GuglielmiA family of tautologies that hold in most logics can be used, following a simple recipe, to produce deductive systems where all rules are local, including cut.27 October 2002

• Goodness, Perfection and MiraclesAlessio GuglielmiI argue about three properties closely related to cut elimination and interpolation theorems. 18 October 2002

• Freedom from BureaucracyFF15 February 1963

5Mailing List

There is a very friendly mailing list devoted to deep inference, proof nets, structads, the calculus of structures and other amphibians of structural proof theory, named Frogs. Join it!

6Grants

These are the current and recent grants I am aware of, regarding deep inference:

• The Fine Structure of Formal Proof Systems and their Computational Interpretations (FISP)2016–2019. Three-year ANR-FWF project at Université Paris Diderot/PPS, INRIA Saclay/École Polytechnique, University of Innsbruck, Vienna University of Technology. 690,647 EUR. Coordinator is Michel Parigot.

• Efficient and Natural Proof Systems2013–2016. Three-year EPSRC research project at University of Bath. 756,061 GBP (full economic costing, including indexation and a research studentship funded by the University of Bath). Principal investigator is Alessio Guglielmi, co-investigator is Guy McCusker.

• Sharing and Sequentiality in Proof Systems with Locality2012–2014. Two-year Royal Society International Exchanges Scheme. Exchange programme between University of Bath and Università di Torino. The two sides get 11,960 GBP. Principal investigators: Alessio Guglielmi and Luca Roversi.

• Extending the Realm of the Curry-Howard Correspondence2011–2012. French-Swiss Academic Research Collaboration Programme (PAI Germaine De Stael). Exchange programme between INRIA Futurs and IAM, Universität Bern. The two sides get around 4,300 EUR each. Principal investigators: Lutz Straßburger and Kai Brünnler.

• Structural and Computational Proof Theory (Structural)2010–2012. ANR—Programme Blanc International/FWF 2010. Three-year project at PPS, LIX, Innsbruck and Vienna. The project gets 441,229 EUR, out of a total cost in France of 2,032,556 EUR, from the Agence Nationale de la Recherche and it gets 291,577 EUR from the FWF. Coordinator and principal investigator is Michel Parigot.

• REDO: Redesigning Logical Syntax2009–2010. INRIA—Action de Recherche Collaborative. Two-year project of the teams Calligramme/Démosthène and Parsifal (INRIA) and the Computer Science Department of the University of Bath. The project gets 80,000 EUR. Principal investigators are Alessio Guglielmi, François Lamarche and Lutz Straßburger (coordinator).

• Identity and Geometric Essence of Proofs (Démosthène)ANR—Chaire d’excellence 2008–2010. Two-year project at LORIA. The project gets about 355,000 EUR from the Agence Nationale de la Recherche, out of a total cost of 750,448 EUR, the rest of which is covered by INRIA. Principal investigator is Alessio Guglielmi.

• Complexity and Non-Determinism in Deep Inference2007–2008. 17 month project at University of Bath. 118,072 GBP, out of a total cost of 147,591 GBP, from the Engineering and Physical Sciences Research Council (EPSRC) Principal investigator is Alessio Guglielmi, co-investigator is Paola Bruscoli.

• Deep Inference and the Essence of Proofs2007–2008. French-Swiss Academic Research Collaboration Programme (PAI Germaine De Stael). Exchange programme between INRIA Futurs and IAM, Universität Bern. The two sides get around 5,000 EUR each. Principal investigators: Lutz Straßburger and Kai Brünnler.

• The Realm of Cut Elimination2007–2008. French-Austrian Academic Research Collaboration Programme (PAI Amadeus). Exchange programme between INRIA Futurs and Theory and Logic Group, Technische Universität Wien. The two sides get around 5,000 EUR each. Principal investigators: Lutz Straßburger and Agata Ciabattoni.

• Theory and Application of Deep Inference (Infer)ANR—Programme Blanc 2006. Three-year project at LIX, LORIA and PPS. The project gets 230,400 EUR, out of a total cost of 1,280,598 EUR, from the Agence Nationale de la Recherche. Coordinator and principal investigator is Lutz Straßburger, other principal investigators are François Lamarche and Michel Parigot.

• Analyticity and Proof Search for Modal Logics in Deep Inference2006–2008. British-German Academic Research Collaboration Programme. Two-year exchange programme between the University of Bath and the Technische Universität Dresden. Bath gets 2,650 GBP from the British Council (principal investigator Alessio Guglielmi) and Dresden gets 5,694 EUR from the German Academic Exchange Service (principal investigator Steffen Hölldobler).

• New Deductive Systems, Normalisation Methods and Semantics for Deep Inference2006–2007. Alliance—Franco-British Partnership Programme. Two-year exchange programme between the University of Bath and the PPS group in Paris. Bath gets 4,300 GBP from the British Council (principal investigator Alessio Guglielmi) and PPS gets 6,250 EUR from the French MAE and the Ministry of Research (principal investigator Michel Parigot).

I did not indicate individual travel grants.

7Beans

• Journals and chapters in books41
•  In press 3 Journal of Logic and Computation (2), Logical Methods in Computer Science 2015 3 Mathematical Logic and Foundations; Logical Methods in Computer Science; ACM Transactions on Computational Logic 2014 3 Categories and Types in Logic, Language, and Physics; Logical Methods in Computer Science; Notre Dame Journal of Formal Logic 2013 2 Logical Methods in Computer Science; ACM Transactions on Computational Logic 2012 4 Annals of Pure and Applied Logic (3); Applied Categorical Structures 2011 5 Mathematical Structures in Computer Science; Journal of Logic and Computation; ACM Transactions on Computational Logic; Logical Methods in Computer Science; Logic without Frontiers (Festschrift for Walter Alexandre Carnielli) 2009 6 ACM Transactions on Computational Logic; Electronic Notes in Theoretical Computer Science; Journal of Logic and Computation; Annals of Pure and Applied Logic; Information and Computation; Archive for Mathematical Logic 2008 3 Annals of Pure and Applied Logic; Logical Methods in Computer Science; Journal of Logic and Computation 2007 5 ACM Transactions on Computational Logic; Studia Logica; Journal of Logic and Computation; Theory and Applications of Categories (2) 2006 5 Studia Logica; Annals of Pure and Applied Logic; Logical Methods in Computer Science (2); Notre Dame Journal of Formal Logic 2003 2 Logic Journal of the IGPL; Theoretical Computer Science
• Conferences56
•  2015 1 RTA 2014 4 CSL-LICS (3), AiML 2013 6 FoSSaCS, LICS, RTA, CSL (2), LPAR 2012 4 CiE, AiML (2), JELIA 2011 3 TLCA, Tableaux, CSL 2010 7 LPAR (2), RTA, LICS, CiE, AiML (2) 2009 5 Tableaux (2), WoLLIC, TLCA, TbiLLC 2008 3 LATA, LPAR, AiML 2007 1 RTA 2006 4 AiML, CiE, LPAR (2) 2005 5 WoLLIC, Logica Universalis, TLCA, AIA, LICS 2004 4 AiML, CSL (2), ISCIS 2003 4 CSL, FOL75, WoLLIC (2, one of which invited talk) 2002 3 LPAR (2), ICLP 2001 2 LPAR, CSL
• Habilitation theses2
•  2011 1 Lutz Straßburger 2010 1 Kai Brünnler
• PhD theses8
•  2013 2 Nicolas Guenot, Anupam Das 2011 1 Linda Postniece 2009 1 Tom Gundersen 2006 2 Richard McKinley, Ozan Kahramanoğulları 2003 2 Kai Brünnler, Lutz Straßburger
• MSc theses4
•  2007 1 Benjamin Robert Horsfall 2005 1 Robert Hein 2004 1 Phiniki Stouppa 2001 1 Alwen Tiu

8Events

Deep inference was one of the main attractions at the following international events:

Deep inference has been taught at

9TeX Macros and BibTeX database

The Virginia Lake LaTeX macros help typing deep inference structures, derivations and atomic flows.

The DedStraker TeX macros are now obsolete.

This BibTeX database of deep-inference publications is kept updated.

18.11.2015Alessio Guglielmiemail