[msp-interest] [MSP101] Robert Atkey: Semantic proofs of Cut-elimination for Deep Infererence (LT412, 3pm Mon 24-Feb)

[Dilsat Yuksel]

Hello,

On Monday, the MSP101 talk will be given by Robert Atkey (MSP). See the details of the talk below.

Best,
Dilsat

**********************************************************************

Date: Monday, 24 February at 15:00

Room: LT412, Livingstone Tower

Zoom link: https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1

Speaker: Robert Atkey

Title: Semantic proofs of Cut-elimination for Deep Infererence

Abstract: Deep Inference systems are a kind of proof calculus that allow inference rules to be applied anywhere in a formula. Cut-elimination for these systems is similar to that for Sequent calculi: rules that introduce intermediate formulas can be removed from proofs. Prior proofs of cut-elimination relied on intricate syntactic method. I'll talk about a semantic approach that builds a model of the whole calculus from cut-free proofs, such that every proof constructed in this model can be read back as a cut-free proof. This is a similar technique to the one used in Normalisation by Evaluation (NbE). The technique is very flexible and extends to many extensions of Multiplicative Linear Logic, including BV's self-dual non-commutative before connective, additives, and exponentials.

This is joint work with Wen Kokke and was published at MFPS last year: https://bentnib.org/sem-cut-elim-mfps.html

**********************************************************************
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.strath.ac.uk/archives/msp-interest/attachments/20250220/37a5b2ed/attachment.html