Go to the first, previous, next, last section, table of contents.
While the underlying type theory has not changed, the Twelf
implementation differs from older Elf implementation in a few ways.
Mostly, these are simplifications and improvements. The main feature
which has not yet been ported is the Elf server interface to Emacs.
Also, while the type checker is more efficient now, the operational
semantics does not yet incorporate some of the optimizations of the
older Elf implementations and is therefore slower.
- Syntax (see section 3 Syntax)
-
The quote `'' character is no longer a special character in the
lexer, and `=' (equality) is now a reserved identifier. The syntax
of
%name declarations has changed by allowing only one preferred
name to be specified. Also, %name, %infix, %prefix
and %postfix declarations must be terminated by a period `.'
which previously was optional. Further, single lines comments now must
start with `%whitespace' or `%%' in order to avoid
misspelled keywords of the form `%keyword' to be ignored.
- Type theory
-
Elf 1.5 had two experimental features which are not available in
Twelf: polymorphism and the classification of type as a type.
- Definitions (see section 3.3 Definitions)
-
Twelf offers definitions which were not available in Elf.
- Searching for definitions (see section 5.2 Solve Declaration)
-
Elf had a special top-level query form
sigma [x:A] B which
searched for a solution M : A and then solved the result of
subsituting M for x in B. In Twelf this
mechanism has been replaced by a declaration %solve c : A which
searches for a solution M : A and then defines c = M : A,
where the remaining free variables are implicitly universally
quantified.
- Query declarations (see section 5.1 Query Declaration)
-
Twelf allows queries in ordinary Elf files as `%query'
declarations. Queries are specified with an expected number of
solutions, and the number of solutions to search for, which can be used
to test implementations.
- Operational semantics (see section 5.5 Operational Semantics)
-
Twelf eliminates the distinction between static and dynamic
signatures. Instead, dependent function types
{x:A} B
where x occurs in the normal form of B are treated
statically, while non-dependent function type A -> B or
B <- A or {x:A} B where x does not occur
in B are treated dynamically.
- Modes (see section 7 Modes)
-
Twelf offers a mode checker which was only partially supported in Elf.
- Termination (see section 8 Termination)
-
Twelf offers a termination checker which can verify that certain
programs represent decision procedures.
- Theorem prover (see section 9 Theorem Prover)
-
Although very limited at present, an experimental prover for theorems
and meta-theorems (that is, properties of signatures) is now available.
It does not yet support lemmas or meta-hypothetical reasoning, which
are currently under development.
- Emacs interface (see section 12 Emacs Interface)
-
The Elf mode has remained basically unchanged, but the Elf server
interface has not yet been ported.
Go to the first, previous, next, last section, table of contents.