Workshop: Twenty Years of Deep Inference

Deep inference is paradigm for designing deductive proof systems. The inference rules in such systems can perform arbitrary rewriting inside formulas. This is very different from what one would expect from more traditional formalisms, like sequent calculus or natural deduction, where formulas are always decomposed along their main connective.

On one side, this provides much more freedom in the design of proof systems, and on the other side this causes a massive breakdown of all important proof theoretical results. Consequently, the early reasearch in deep inference went into reestablishing traditional results, like cut elimination, that one would expect from a deductive proof system.

After that many new results for deep inference have been obtained in recent years, in particular:

• proof systems for logics that cannot be expressed in traditional sequent systems,
• proof systems whose inference rules are all local,
• new notions of normalizations, in addition to cut elimination or focusing,
• to type optimal versions of the lambda-calculus that are typable with traditional formalisms,
• shorter analytic (cut-free) proofs by exponential factors (compared to Gentzen systems).

Besides that, deep inference inspired new notions of proof nets and semantics for proofs, and new research in proof complexity.

The purpose of this workshop is to present this vast growing field in a coherent, easy accessible way to other communities in all areas of logic in computer science, and bring together researchers in the area of deep inference to exchange ideas and to discuss their current work.

An up-to-date bibliography on deep inference can be found here.

Alessio Guglielmi (University of Bath)
Willem Heijltjes (University of Bath)
Anupam Das (University of Copenhagen)
Dominic Hughes (UC Berkeley)

We accept work in progress as well as already published/submitted work. However, we do not allow work that is presented at another FLoC 2018 event.

Contributions should consist of an abstract of 1-3 pages in pdf-format and be submitted via this EasyChair page.

Via the FLoC registration web page.

Submission Deadline: 15 April 2018
Notification: 15 May 2018
Final Version: 25 May 2018
Early Registration: June 6 2018
Workshop: 7 July 2018

Time	Saturday 7 July 2018
08:30-09:00	Setup (help desk available)
09:00-10:00	Willem Heijltjes: An introduction to deep inference
10:00-10:30	Joseph Paulus: Deep-Inference Intersection Types (paper)
10:30-11:00	Coffee
11:00-11:30	Ross Horne: Truely Concurrent Processes in the Calculus of Structures
11:30-12:00	Elaine Pimentel: Sequentialising nested systems
12:00-12:30	Sonia Marin: Nested sequents for modal logics and beyond
12:30-14:00	Lunch
14:00-15:00	Alessio Guglielmi: Two Unifying Structural Principles
15:00-15:30	Benjamin Ralph: Deep Inference, Herbrand's Theorem and Expansion Proofs
15:30-16:00	Coffee
16:00-17:00	Dominic Hughes: Some incoherent musings on deep inference and combinatorial proofs
17:00-18:00	Anupam Das: Proof complexity of deep inference: a survey
18:00-19:00	Open Discussion

The workshop is part of FLoC 2018.

Andrea Aler-Tubella
Lutz Straßburger