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 - Rocquencourt Amphi Turing du bâtiment 1 Lundi 27 avril, 10h30 ------------------- Beniamino Accattoli ------------------- INRIA =============================================== Lambda Calculus, Invariance, and Useful Sharing =============================================== As a computational model lambda-calculus does not come with a notion of machine, that is both its advantage (for clean specifications) and its drawback (as there are no evident cost models). In this talk I will survey three recent joint works of mine, based on a new simple approach to explicit substitutions---the Linear Substitution Calculus (LSC)---providing cost models and easy complexity analysis for lambda-calculus: 1) a simulation of the ordinary (strong) lambda calculus by Turing machines having only a polynomial overhead, solving a long standing open problem (the 'invariance' of lambda calculus wrt reasonable computational models) and relying on the new notion of 'useful sharing' (A. & Dal Lago, CSL-LICS 2014); 2) a modular decomposition of most abstract machines for call-by-name/value/need into the LSC, together with a linear bound of their overhead wrt the number of beta steps (A. & Barenbaum & Mazza, ICFP 2014); 3) an abstract machine implementing useful sharing for a core call-by-value language, having only linear overhead wrt to the number of betas (A. & Sacerdoti Coen, LICS 2015).