Seminar

!! The seminar was moved to 16:30 !!
Thursday, July 2nd, 2020, 16:30, on Zoom.

Gianluigi Bellin (Università di Verona)
Relational sequent calculus for Bi-Intuitionistic Linear Logic (j.w.w. W. Heijltjes)

Abstract: The relational sequent calculus for BILL used in [Bellin & Heijltjes, {Proof nets for bi-intuitionistic linear logic}, FSCD 2018] is unsound. The problem extends to Hyland and De Paiva Full Iintuitionistic Linear Logic FILL 1993, but only to the treatment of the unit ⊥, as shown by an example of failure of interpolation in the sequent calculus, which yields unsoundness with respect to Hyland and De Paiva’s categorical semantics. We revise the sequent calculus, sketch the proof of interpolation and of cut elimination for it.

The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster.