[msp-interest] [MSP101] Zanzi Mihejevs: A canonical bidirectional typing discipline through polarised System L (LT412, 3pm Mon 10-Mar)

[Dilsat Yuksel]

Hi,

On Monday, the MSP101 talk will be given by Zanzi Mihejevs (GlAiVe Research). See the details of the talk below.

Best,
Dilsat

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

Date: Monday, 10 March at 15:00

Room: LT412, Livingstone Tower

Zoom link: https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1
Live stream on Youtube: https://www.youtube.com/@msp101strathclyde4

Speaker: Zanzi Mihejevs

Title: A canonical bidirectional typing discipline through polarised System L

Abstract: What is the relationship between polarity and bidirectional typing? It has long been observed that there is a connection between the two, but the precise relationship has remained unclear. Moreover, it has been argued that the link itself is a red herring, and that bidirectional typing is better explained not by polarity but by chirality - the duality between producers and consumers.
In this talk we will look at Polarised System L, a type theory that combines both dualities - the positive fragment is driven by a cut between a primitive producer and a pattern, and the negative fragment is driven by a cut between a primitive consumer and a co-pattern.
Remarkably, linear System L admits a canonical bidirectional typing discipline based on a combination of ideas from both standard and co-contextual typing, giving us a bi-contextual typing algorithm.
We will see how this lets us equip a type system based on full classical linear logic - containing all four connectives and derivable implication and co-implication - with a bidirectional discipline where all typing annotations are exclusively limited to shifts between sythesisable and checkable expressions.

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.strath.ac.uk/archives/msp-interest/attachments/20250307/0fdac882/attachment.html