TY - GEN
T1 - Functional programming with λ-tree syntax
AU - Gérard, Ulysse
AU - Miller, Dale
AU - Scherer, Gabriel
N1 - Publisher Copyright:
© 2019 ACM.
PY - 2019/10/7
Y1 - 2019/10/7
N2 - 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.
AB - 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.
U2 - 10.1145/3354166.3354177
DO - 10.1145/3354166.3354177
M3 - Conference contribution
AN - SCOPUS:85083401314
T3 - ACM International Conference Proceeding Series
BT - Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
PB - Association for Computing Machinery
T2 - 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
Y2 - 7 October 2019 through 9 October 2019
ER -