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.

• 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 typetheory_paper.pdf.
• 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.

The Twelf system can be used without installing it on your local machine by using the Twelf Live Server.