Delphin Details

Intro

Delphin is a robust dependently-typed programming language supporting higher-order encodings.

Source Code

• • Github repo: https://github.com/aposwolsky/delphin

    • Under code/delphin

• Delphin Source available (v 1.5.1, Released April 2008): delphin-1.5.1.tar.gz.

  • Termination-Checker included (lexicographic order of all explicit inputs)

  • Coverage Checker implements rules in Dissertation below.

  • Compare: Converted examples involving First-order Logic from Twelf (fol.elf) into Delphin Version (fol.d).

• compiled in SML/NJ v110.65

• Delphin Examples

  • Compare to Elphin Examples

  • An example of Hindley-Milner type inference is available using parameters instead of the typical references.

    • Available here (Warning: this is an advanced example).

Documents

• Dissertation (includes user manual for Delphin):

  • Adam Poswolsky. Functional Programming with Logical Frameworks: The Delphin Project, Ph.D. Dissertation, CreateSpace, 2008. ISBN 978-1440474927 (PDF, Amazon).

    • Simply-Typed Examples

    • Dependently-Typed Examples

    • Advanced Example

• Adam Poswolsky and Carsten Schürmann. System Description: Delphin – A Functional Programming Language for Deductive Systems. In International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP ’08), Electronic Notes in Theoretical Computer Science (ENTCS), pages 135–141, Pittsburgh, PA, June 2008. Elsevier. (PDF)

• Adam Poswolsky and Carsten Schürmann. Practical Programming with Higher-Order Encodings and Dependent Types. In European Symposium on Programming (ESOP 2008), pages 93–107, Budapest, Hungary, 2008. ISBN 978-3-540-78738-9.

  • Full Version (PDF)

  • Extended Technical Report, YALEU/DCS/TR-1375 (PDF)

  • Example file from Paper: esop08.d

Earlier Design of Delphin

• Adam Poswolsky. A Temporal-Logic Approach to Functional Calculi for Dependent Types and Higher-Order Encodings, YALEU/DCS/TR-1364, 2006.

  • Full Version (PDF)

  • Extended Technical Report (PDF)

  • Twelf Code (.tar.gz)

Related

• Miller and Tiu, A Proof Theory for Generic Judgments: An extended abstract. (PDF)

  • Here they present their own ∇ constructor which they use to distinguish between eigenvariables intended for instantiation from those representing scoped constants. Their reasoning occurs over formulas with an explicit local context of scoped constants. In our setting there is only a global context, which renders it more useful for functional programming.

• Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions (POPL 2008)

  • Here they present a simply-typed system also designed to reason over higher-order encodings. Their approach is quite opposite to our approach. Whereas we aim to keep meta-level constructs such as context and substitution implicit, they make them explicit objects that the programmer must use. For example, they introduce the abstraction and application of explicit context variables. Our approach avoids this by only addressing the "relative" difference in the context using our ∇ type constructor. They acknowledge the problem of having explicit context variables and defer the reconstruction of context variables to future work.

• Dependent Types:

  • There are many other systems that have addressed programming with some form of Dependent Types. Please see the paper here for a more detailed explanation. However, they stop short of supporting higher-order encodings.

• Freshness:

  • Our work is also related to programming languages with freshness, such as FreshML. They allow for limited support of higher-order abstract syntax as substitution must still be explicit, albeit easier to write. In their work the creation of a fresh parameter is a global effect. Interestingly, there is recent work by Pottier used to prove that names do not escape their scope. However, in our system the creation of parameters is not a global effect and scoping is guaranteed by typing.

    • François Pottier. Static name control for FreshML. In LICS'07.

Selected Publications regarding the Meta Logical Framework Twelf

• [S01a] Carsten Schürmann. Recursion for Higher-Order Encodings. Proceedings of Computer Science Logic (CSL 2001), Paris, France. LNCS 2142, pp 585-599, 2001

• [S00b] Carsten Schürmann. Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, 2000. CMU- CS-00-146

• [S00a] Carsten Schürmann. A Meta Logical Framework Based on Realizability. Workshop on Logical Frameworks and Meta-Languages (LFM 2000), Santa Barbara, California, June 2000.

• [PS99] Frank Pfenning and Carsten Schürmann. System description: Twelf --- a meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202--206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632.

• [SP98] Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 286--300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421.