Sciweavers

Share
ENTCS
2007

Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions

8 years 6 months ago
Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions
syntax and explicit substitutions Brigitte Pientka1 School of Computer Science McGill University Montreal, Canada This paper sketches a foundation for programming with higher-order abstract syntax and explicit substitutions based on contextual modal type theory [NPP05]. Contextual modal types not only allows us to cleanly separate the representation of data objects from computation, but allow us to recurse over data objects with free variables. In this paper, we extend these ideas even further by adding first-class contexts and substitutions so that a program can pass and access code with free variables and an explicit environment, and link them in a type-safe manner. We sketch the static and operational semantics of this language, and give several examples which illustrate these features.
Brigitte Pientka
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Brigitte Pientka
Comments (0)
books