Objective

The objective of this research is to develop a novel programming method that embraces logical framework technology at its core. To achieve this goal we propose to design and implement a programming language called Delphin that allows users to program with proofs, theorems, algorithms, code, and in general all kind of knowledge and its properties as if they were numbers, lists, trees, or arrays. The representation is direct and elegant, because common concepts such as environments, variables, substitutions and so on are implicitly provided and need not be explicitly programmed. Delphin will have the following features:

Delphin

Delphin has been an ongoing project for many years.  We have experimented with many different possibilities (available here), culminating in an elegant logically-motivated system with a ∇-construct similar to, albeit different from, Miller's.

What's  New

Related

Elphin

Towards this end, we first rigorously designed and implemented the ∇-calculus, a calculus for defining general recursive functions over higher-order encodings.  Elphin is limited to the simply-typed fragment and follows a more ad-hoc stack-based solution which did not extend well to dependent-types.