Sites Inria

Version française

Research team 's seminary

Ulysse Gérard : Functional programming with lambda-tree syntax

© INRIA Sophie Auvin - G comme Grille

We present the design of a new functional programming language, MLTS, that possesses built-in mechanisms for treating data structures that include bindings.

  • Date : 12/03/2018
  • Place : Inria Paris - 2 rue Simone Iff- 75012 - Paris- Salle Lions 1- bâtiment C
  • Guest(s) : Ulysse Gérard ( Inria Saclay)

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.

Keywords: Galium Research team Seminary Inria Paris

Top