Séminaire des équipes Gallium
Inria - Paris
2 rue Simone Iff 75012 Paris
Salle Lions 1, bâtiment C
15 octobre, 10h30
- Date : 15/10/2018
- Lieu : Salle Lions 1, bât C
- Intervenant(s) : Kenji Maillard
- Organisateur(s) : Gallium
An introduction to polarised L calculi
L calculi , so-named after Gentzen's LK and LJ, have evolved from Curien-Herbelin's λμ̃μ by further integrating the contributions from proof theory such as focalisation and polarisation (Andreoli, Girard, …). These calculi restrict the reduction rules according to a type- or polarity-based evaluation order. Like Call-By-Push-Value, polarized calculi are an interesting vehicle to study side-effects, since they can encode and mix both call by name and call by value. However L caluli reveal the importance of linearity and thunkability, two generalizations of the idea of purity, when dealing with side-effects.
This presentation stems from an effort to write an accesible tutorial to these notions. After recalling the syntax and semantics of μ̃μ, we will explain how we introduce polarization in this setting. L calculi also admit extensions with side-effects in a rather uniform fashion and we will use this possibility to illustrate properly the notions of linearity and thunkability.