View: session overviewtalk overviewside by side with other conferences

09:00 | 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. |

10:00 | SPEAKER: Joseph Paulus ABSTRACT. We explore the formulation of non-idempotent intersection types for the lambda-calculus in deep-inference using the open-deduction formalism. |

11:00 | 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. |

11:30 | SPEAKER: Elaine Pimentel 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. |

12:00 | 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. |

Workshops dinner at Balliol College. Drinks reception from 7.45pm, to be seated by 8:15 (pre-booking via FLoC registration system required; guests welcome).