Functional programming with λ-tree syntax: a progress report

Authors: Ulysse Gérard and Dale Miller

Paper Information

Title:Functional programming with λ-tree syntax: a progress report
Authors:Ulysse Gérard and Dale Miller
Proceedings:LFMTP Regular papers
Editors: Giselle Reis and Frédéric Blanqui
Keywords:binder mobility, lambda-tree syntax, functional programming, Abella

ABSTRACT. In this progress report, we highlight the design of the functional programming language MLTS which we have recently proposed elsewhere. This language uses the λ-tree syntax approach to encoding data structures that contain bindings. In this setting, bound variables never become free nor escape their scope: instead, binders in data structures are permitted to move into binding sites within programs. The concrete syntax of MLTS is based on the one for OCaml but includes additional binders within programs that directly support the mobility of bindings. The natural semantics of MLTS can be viewed as a logical theory within the logic G, which forms the basis of the Abella proof system and which includes nominal abstractions and the ∇-quantifier. Here, we provide several examples of MLTS programs. We also illustrate how many Abella relational specifications that are known to specify functions can be rewritten as functions in MLTS.

Talk:Jul 07 17:30 (Session 31H: Implementation)