Workshop: Twenty Years of Deep Inference

Oxford, 7 July 2018

Overview

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:

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.

Invited Speakers

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

Submission Instructions

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.

Registration

Via the FLoC registration web page.

Important Dates

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

Participants

TBA

Programme

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

Venue

The workshop is part of FLoC 2018.

Organization

Andrea Aler-Tubella
Lutz Straßburger