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 12 mars, 10h30 ------------- Ulysse Gérard ------------- Inria Saclay ============================================== Functional programming with lambda-tree syntax ============================================== We present the design of a new functional programming language, MLTS, that possesses built-in mechanisms for treating data structures that include bindings. We employ the lambda-tree syntax approach (a style of HOAS) which means that bindings can move between data structures and programming language features: bound variables never become free or escape their scope. To achieve that goal, MLTS adds sites within programs that directly support the movement of bindings. The natural semantics of MLTS is given in a rich logic that extends Church's Simple Theory of Types with both nabla-quantification and nominal abstraction, both of which are part of the logic underlying the Abella prover. The rich binding structures supported by this logic and its proof theory makes it possible to give a direct and elegant natural semantics specification. We provide several example programs.