Summer school 2008

From The Twelf Project
Jump to: navigation, search

This page contains course materials for the Twelf course at the University of Oregon Summer School on Logic and Theorem Proving in Programming Languages, July 2008. In this course, you will learn to represent deductive systems in LF and prove metatheorems about them with Twelf.

New: Feedback Form

Please fill out our feedback form!

Get Twelf

Pre-built binaries of Twelf are available for most operating systems through the Twelf Night(ly).


  • you can build Twelf from the source tarball. You will need MLton or sml/nj.
  • you can make yourself an account on the wiki, and do the exercises on your User:<login> page (linked at the top after you log in).

Then see Twelf with Emacs for the basics of interacting with Twelf. (You can also use Twelf without Emacs, by interacting with the Twelf server directly.)

Lectures and Labs (slides)

Class 1: Overview

Class 2: Representation

Class 3: Mechanizing Metatheory

Additional reading