Practical Programming with Higher-Order Encodings and Dependent Types

Adam Poswolsky, Carsten Schürmann

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftKonferenceartikelForskningpeer review


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 Miller and Tiu’s ∇-quantifier [1].
BogserieLecture Notes in Computer Science
Sider (fra-til)93-107
StatusUdgivet - 2008
Begivenhed17th European Symposium on Programming, ESOP 2008 - Budapest, Ungarn
Varighed: 29 mar. 20086 apr. 2008
Konferencens nummer: 17


Konference17th European Symposium on Programming, ESOP 2008