Delphin (Dolphin)The Delphin Project

 

horizontal rule

Home
Downloads
Publications
Contact Us

Why?

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

bullet

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

Simply-Typed Examples

bullet

Dependently-Typed Examples

bullet

Advanced Example

bullet

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.

 
bullet

Runnable Implementation of Elphin is available, including many examples.

 

Acknowledgements

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 poswolsky@cs.yale.edu.
Last updated: 02/09/09.