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. |
|
The Delphin page contains publications, source code,
manuals, and examples. What's New
|
