Skip to Main content Skip to Navigation
Conference papers

Functional programming with λ$-tree$ syntax: a progress report

Ulysse Gérard 1 Dale Miller 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-01806129
Contributor : Ulysse Gérard <>
Submitted on : Friday, June 15, 2018 - 5:44:48 PM
Last modification on : Friday, April 30, 2021 - 10:02:39 AM
Long-term archiving on: : Monday, September 17, 2018 - 12:10:33 PM

File

paper (1).pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01806129, version 2

Collections

Citation

Ulysse Gérard, Dale Miller. Functional programming with λ$-tree$ syntax: a progress report. 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2018, Oxford, United Kingdom. ⟨hal-01806129v2⟩

Share

Metrics

Record views

400

Files downloads

213