Copenhagen Programming Language Seminar

Functional Programming with Higher-Order Abstract Syntax and Dependent Types

Adam Poswolsky
Yale University

Monday, September 22, 2008, 15:00-16:00
ITU, Rued Langgaards Vej 7, 2300 Copenhagen S. Room: 2A.12


In this talk I present the Delphin programming language, which is a functional programming language supporting both higher-order abstract syntax and dependent types. Higher-order abstract syntax, or HOAS, refers to the technique of representing variables of an object language using variables of a meta language, which leads to more concise and elegant encodings than first-order alternatives. Dependent types allow one to represent complex data (such as derivations in various logics) and enforce more properties of programs than possible using only simple types.

Delphin is not only a useful programming language but also a useful system for formalizing proofs as total functions express proofs that the input entails the output. Just as representations using HOAS free the programmer from concerns of handling explicit contexts and substitutions, our system permits computation and reasoning over such encodings without making these constructs explicit, leading to concise and elegant programs. Delphin is a two-level system distinguishing functions used for representation from functions expressing computation. The ability to perform computation over higher-order data is driven by a construct allowing the dynamic introduction of scoped constants, which we call parameters.

I will motivate the Delphin system with examples. Related publications, source code, and examples can be found at http://www.delphin.logosphere.org/

Scientific host:Carsten Schürmann Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org