The Delphin Project

 

Department of Computer Science
Yale University
51 Prospect St.
New Haven, CT 06520-8285
U.S.A.
 

  Home
  Publications
 

News

An extended version of the paper "Towards functional programming with logical frameworks" is available here.

An experimental and incomplete implementation of Delphin is available. But it is not available for download yet. Please contact carsten@cs.yale.edu directly for further information.

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:
  • It will be based on the the logical framework LF. One goal is to design Delphin in such a way that it can be easily extended to other logical frameworks in the future.
  • It will be able to handle effects such as exceptions and state.
  • It will have a sound type system and an appropriate operational semantics.
  • It will be implemented in Standard ML.

Members of the team

Carsten Schürmann
Andrew McCreight
Sebastian Nanz
Yu Liao (on leave)
Adam Poswolsky
Jeffrey Sarnat

Former Members

Richard Fontana
Kevin Redwine (Visitor from the University of Oregon)

Acknowledgements

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