Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                           Lundi 15 octobre, 10h30

                                --------------
                                Kenji Maillard
                                --------------

                                 Inria Paris

                    ======================================
                    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.