Functional Programming with lambda-tree syntax
We present the design of a new functional programming language, MLTS, that possesses built-in mechanisms for treating data structures that include bindings. We employ the lambda-tree syntax approach (a style of HOAS) which means that bindings can move between data structures and programming language features: bound variables never become free or escape their scope. To achieve that goal, MLTS adds sites within programs that directly support the movement of bindings. The natural semantics of MLTS is given in a rich logic that extends Church's Simple Theory of Types with both nabla-quantification and nominal abstraction, both of which are part of the logic underlying the Abella prover. The rich binding structures supported by this logic and its proof theory makes it possible to give a direct and elegant natural semantics specification. We provide several example programs.
Joint with Ulysse Gerard and Gabriel Scherer.
On line demo: https://trymlts.github.io/
Draft paper: https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mlts-draft-nov-...
Speaker Bio: Professor Dale Miller received his PhD in Mathematics in 1983 from Carnegie Mellon University. He has been a professor at the University of Pennsylvania and Ecole Polytechnique (France) and Department Head in Computer Science and Engineering at Pennsylvania State University. He has held visiting positions at the Australian National University and the universities of Aix-Marseille, Sienna, Genoa, Pisa, and Edinburgh. He is currently Director of Research (classe exceptionnelle) at Inria Saclay where he is the Scientific Leader of the Parsifal team. Miller works on various topics in computational logic including proof theory, automated reasoning, logic programming, unification theory, operational semantics, and proof certificates.His work in these areas is well-recognized. Amongst other things, he has been awarded a prestigious ERC Advanced Grant and two of his papers have won the LICS Test-of-Time awards.