I first, briefly, present the syntax of MuLL which is an extension of David Baelde’s MuMALL (multiplicative and additive linear logic with least and greatest fixpoints) with exponentials. Then we will study the categorical model of Mu LL and provide two concrete models of MuLL based and REL (sets and and relation) and NUTS (non uniform totality spaces) which are sets equipped with a notion of totality and a relation preserving it. Then we will study a polarized version of muLL, and will try to develop a calculus based on this polarized version, called mu LLP. We equip this language with a deterministic reduction semantics as well as a denotational semantics based on NUTS. Finally, We prove an adequacy result between these operational and denotational semantics, from which we derive a normalization property for mu LLP thanks to the properties of the totality interpretation.

This presentation is based on joint work with Thomas Ehrhard and Alexis Saurin.