# Functional programming with $λ$-tree syntax

1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : We present the design of a new functional programming language, MLTS, that uses the $λ$-tree syntax approach to encoding bindings appearing within data structures. In this approach, bindings never become free nor escape their scope: instead, binders in data structures are permitted to move to binders within programs. The design of MLTS includes additional sites within programs that directly support this movement of bindings. In order to formally define the language's operational semantics, we present an abstract syntax for MLTS and a natural semantics for its evaluation. We shall view such natural semantics as a logical theory within a rich logic that includes both nominal abstraction and the $∇$-quantifier: as a result, the natural semantics specification of MLTS can be given a succinct and elegant presentation. We present a typing discipline that naturally extends the typing of core ML programs and we illustrate the features of MLTS by presenting several examples. An on-line interpreter for MLTS is briefly described.
Keywords :
Document type :
Conference papers
Complete list of metadata

Cited literature [60 references]

https://hal.inria.fr/hal-02368906
Contributor : Dale Miller Connect in order to contact the contributor
Submitted on : Tuesday, November 19, 2019 - 11:47:56 AM
Last modification on : Wednesday, February 2, 2022 - 3:55:18 PM
Long-term archiving on: : Thursday, February 20, 2020 - 3:11:15 PM

### File

mlts-2019.pdf
Files produced by the author(s)

### Citation

Ulysse Gérard, Dale Miller, Gabriel Scherer. Functional programming with $λ$-tree syntax. PPDP 2019 - 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-16, ⟨10.1145/3354166.3354177⟩. ⟨hal-02368906⟩

Record views