Time: 1:00 - 2:00pm Venue: QMUL campus, Informatics Technology Lab (ITL) top floor
Title: Concrete fully complete models of Linear Logic
Speaker: Thomas Cuvillier
Time: 13:00-14:00 on Thu 29/03/18
Place: ITL top floor
http://theory.eecs.qmul.ac.uk/seminars/
Abstract
Linear logic is one of the most studied logics in theoretical computer science, especially from the denotational semantics point of view.
Several important models, such as coherence spaces or games, have been first introduced as denotational models for linear logic, before being reused successfully for programming languages. The main goal of the present research is to find a concrete model that is also complete model; property described by Abramsky as "the tightest possible connection between syntax and semantics". Precisely, we want to avoid the use of 2-categorical tools to model type variables, together with not relying on a quotient. We hope that such a model could provide important insights for the study of linear logic, but also related and connected fields in semantics, such as semantics of programs and processes.
We will first recall the basics of Linear Logic, proof structures, and their associated categorical models. We present a new categorical construction mixing double-glueing and the Chu-construction. We build a relational semantics of proof structures based on permutations. We then use the new categorical construction to restrict the relation category and obtain full completeness for the multiplicative fragment without units. Moreover, our model can be enriched with a hypercoherence structure to yield a static fully complete model for the multiplicative additive fragment without units. This result allows us to prove a conjecture made by Pagani that relates hypercoherence and proof structures.
Directions, if coming from outside QMUL
Queen Mary is on Mile End Road, with nearest tube stations being Stepney Green (closest one to the seminars) and Mile End. The seminars are in the Informatics Teaching Laboratory, floor 2: https://goo.gl/maps/hYgvAwTx76v
As the building has card access, it is best to inform us that you will be coming (email Nikos Tzevelekos).