[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
The Delphin Programming Language: Functional programming over LF ------------------------- Delphin is a functional programming language that utilizes LF for its datatypes. The key difficulties that we address are in supporting computation over higher-order encodings as well as supporting dependent types. When programming in languages like ML, Haskell, or even Twelf, the notion of "context" and "substitution" are meta-level concepts hidden to the programmer and they remain hidden in our system. We support computation over higher-order encodings by distinguishing between two methods of variable binding. A function can be written as fn x => e. This has the standard meaning of a function, where the binding x is intended for instantiation. The computation of e is triggered by application which first instantiates the x. Alternatively, we provide a newness constructor binding variables that will always remain uninstantiated. We write "{<x>}e", and the evaluation of e occurs while the binding x is uninstantiated. Therefore, for the scope of e, the variable x behaves as a fresh constant, which we call a "parameter". Delphin pervasively distinguishes between parameters and objects and typing statically guarantees that parameters cannot escape their scope. A submitted paper describing the underlying calculus of Delphin is at: http://cs-www.cs.yale.edu/homes/delphin/files/popl08-submission.pdf You are invited to try out our implementation available at: http://cs-www.cs.yale.edu/homes/delphin/delphin.htm (You will need SML/NJ or PolyML to install it) We welcome your feedback as well as any questions. There are many examples illustrating Delphin on the website. These examples range from simple addition, to combinator transformations, to an example of type inference using parameters instead of the typical references. Please direct your comments/questions to [EMAIL PROTECTED] . Thank you. Adam Poswolsky [EMAIL PROTECTED]