Le 7 juillet 2012, à 14h en salle B311, le séminaire LCR accueille Alejandro Díaz-Caro (LIPN).
We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F with pairs, which corresponds to a non linear fragment of linear logic. The translation provides a deeper understanding of the linearity in our setting, which we will discuss in this presentation.
Joint work with Barbara Petit. To appear in LNCS ( Proceedings of WoLLIC’12 ). arXiv:1011.3542