Thursday 19 October 2023, 15:00, room 1Z76: Polarized Linear Logic with Fixpoints, Farzad Jafarrahmani (LIP6).

In this talk, I will present a joint work with Thomas Ehrhard and Alexis Saurin on μLLP, which can be viewed both as an extension of Laurent's Polarized Linear Logic, LLP, with least and greatest fixpoints, and as a polarized version of Baelde and Miller’s Linear Logic with fixpoints (μMALL and μLL). We take advantage of the implicit structural rules of μLLP to introduce a term syntax for this language, in the spirit of the classical lambda-calculus and of system L in the style of Curien, Herbelin and Munch-Maccagnoni. We equip this language with a deterministic reduction semantics as well as a denotational semantics based on the notion of non-uniform totality spaces and the notion of categorical model for linear logic with fixpoint. At the end, I will show you an adequacy result for μLLP between these operational and denotational semantics, from which we derive a normalization property for μLLP thanks to the properties of the totality interpretation.