Home
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:
It utilizes the logical framework LF for representation, which supports higher-order abstract syntax (HOAS) and dependent types.
It provides a computation level to manipulate LF data.
It contains meta-level totality checks allowing the programmer to write proofs as the totality of a function entails that the input yields the output.
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).
The Delphin page contains publications, source code, manuals, and examples.
Dissertation (including user manual for Delphin) (Amazon link)
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.