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