Sciweavers

Share
ESOP
2008
Springer

Practical Programming with Higher-Order Encodings and Dependent Types

8 years 8 months ago
Practical Programming with Higher-Order Encodings and Dependent Types
Abstract. Higher-order abstract syntax (HOAS) refers to the technique of representing variables of an object-language using variables of a meta-language. The standard first-order alternatives force the programmer to deal with superficial concerns such as substitutions, whose implementation is often routine, tedious, and error-prone. In this paper, we describe the underlying calculus of Delphin. Delphin is a fully implemented functional-programming language supporting reasoning over higher-order encodings and dependent types, while maintaining the benefits of HOAS. More specifically, just as representations utilizing HOAS free the programmer from concerns of handling explicit contexts and substitutions, our system permits programming over such encodings without making these constructs explicit, leading to concise and elegant programs. To this end our system distinguishes bindings of variables intended for instantiation from those that will remain uninstantiated, utilizing a variation of...
Adam Poswolsky, Carsten Schürmann
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where ESOP
Authors Adam Poswolsky, Carsten Schürmann
Comments (0)
books