Summer school 2008
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!
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).
Lectures and Labs (slides)
Class 1: Overview
- Arithmetic expressions
- Arithmetic expressions with let-binding
- Typed arithmetic expressions
Class 2: Representation
Class 3: Mechanizing Metatheory
- PFPL: We will use Practical Foundations for Programming Languages as a reference for basic PL concepts.
- MMLF: Mechanizing Metatheory in a Logical Framework discusses LF, representation, and mechanized metatheory in technical detail.
- Proving metatheorems with Twelf is a self-contained intro tutorial on this wiki.
- After you get spun up, there are lots of tutorials and case studies.