Twelf is a proof assistant tool for checking and deriving proofs of mathematical properties. The Twelf system provides useful software features, such as higher-order abstract syntax, for reasoning about formal languages and deductive logics.
This package is a tutorial on Twelf and type theory.
Concepts are presented using a Twelf encoding of
programming language Minilang.
Minilang is a language of number and strings
that is rigorously defined in file
typetheory_paper.pdf: Presents a type theory tutorial using Minilang as an example language for presenting concepts.
typetheory_slides.pdf: Slide presentation of material in
twelf_slides.pdf: More detailed slide presentation of Twelf and Twelf encoding of Minilang.
sources.cfg: Tells Twelf the files to read and the order in which to process them.
syntax.elf: Twelf encoding of Minilang's syntax.
typing.elf: Twelf encoding of Minilang's typing rules or static semantics.
evaluation.elf: Twelf encoding of Minilang's evaluation rules or dynamic semantics.
preservation.elf: Contains the preservation theorem and its proof.
progress.elf: Contains the progress theorem and its proof.
test_typing.elf: Provides example judgments that can be automatically derived by Twelf.
Twelf Live Server
The Twelf system can be used without installing it on your local machine by using the Twelf Live Server.