Delphin (Dolphin)The Delphin Project


horizontal rule

Contact Us


The objective of this research was to develop a novel programming method that embraces logical framework technology at its core. To achieve this goal we designed and implemented a functional programming language called Delphin that allows users to program with proofs, theorems, algorithms, etc. as if they were numbers, lists, trees, or arrays. The representation is direct and elegant because common concepts such as environments, variables, and substitutions are implicitly provided and need not be explicitly handled by the programmer.

Delphin has the following features:

bulletIt utilizes the logical framework LF for representation, which supports higher-order abstract syntax (HOAS) and dependent types. 
bulletIt provides a computation level to manipulate LF data.
bulletIt contains meta-level totality checks allowing the programmer to write proofs as the totality of a function entails that the input yields the output.

Delphin Page

The Delphin page contains publications, source code, manuals, and examples.

What's  New


Dissertation (including user manual for Delphin) (Amazon link)

Simply-Typed Examples


Dependently-Typed Examples


Advanced Example


Version 1.5.1 Released (April 2008)

Elphin Page

Elphin is the direct predecessor to Delphin.  Elphin does not support dependent types and deals solely with issues of higher-order abstract syntax (HOAS) and is significantly different than the Delphin system.  It follows a more ad-hoc stack-based solution which did not extend well to dependent types.


Runnable Implementation of Elphin is available, including many examples.



This material is based upon work supported by the National Science Foundation under Grant No. CCR-0133502. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation (NSF).

horizontal rule

Home | Downloads | Publications | Contact Us

For problems or questions regarding this web contact
Last updated: 02/09/09.