University of Minnesota
Master of Science in Software Engineering

You are here

Seminar: Functional programming with lambda-tree syntax

Date of Event: 
Wednesday, June 19, 2019 - 3:00pm to 4:30pm
3-111 Keller Hall, 200 Union Street S.E., Minneapolis, MN 55455

Talk by:   Prof. Dale Miller, Inria Saclay and LIX Ecole Polytechnique, France

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.

Joint with Ulysse Gerard and Gabriel Scherer.

On line demo:

Draft paper:

Host: Prof. Gopalan Nadathur

» Read more and Sign up for event