|
| |
Software
Source Code: Available
Here
 | Latest Version:
Version 1.5.1, April 2008
 | 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
|
| New: July 30th, 2007: An example of Hindley-Milner
type inference is available using parameters instead of the typical
references.
| Available
here. |
| Warning: This is an advanced example. |
|
Papers
Previous Design of Delphin
An alternative recent design has been studied based on Temporal Logic
both utilizing a modal operator and a three-tiered hierarchical system.
The simply-typed version has been formally verified in Twelf.
|
Adam Poswolsky. A Temporal-Logic Approach to
Functional Calculi for Dependent Types and Higher-Order Encodings.
|
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.
|
|
|
|
   |
|
