Practical Programming with Higher-Order Encodings and Dependent Types

Adam Poswolsky, Carsten Schürmann

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-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].
Original languageEnglish
Book seriesLecture Notes in Computer Science
Pages (from-to)93-107
Publication statusPublished - 2008
Event17th European Symposium on Programming, ESOP 2008 - Budapest, Hungary
Duration: 29 Mar 20086 Apr 2008
Conference number: 17


Conference17th European Symposium on Programming, ESOP 2008

Cite this