We present the design of a new functional programming language, MLTS, that uses the λ-tree syntax approach to encoding bindings that appear within data structures. In this setting, bindings never become free nor escape their scope: instead, binders in data structures are permitted to move into binders within programs. The design of MLTS – whose concrete syntax is based on that of OCaml – includes additional sites within programs that directly support the movement of bindings.

In a workshop presentation, we offer to illustrate the features of MLTS by going through several examples. We would also present a typing discipline that naturally extends standard ML type systems, and a natural semantics for MLTS programs.