Summer school 2008

From The Twelf Project

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).

• Linux (tgz)
• Windows (exe)
• Mac OS 10.4 or 10.5 (Intel only) (dmg)

Otherwise:

• 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

• Arithmetic expressions
• Arithmetic expressions with let-binding
  • Variation: Call-by-value let-binding syntax
  • Variation: Defining evaluation with a hypothetical judgement
• Typed arithmetic expressions
  • Variation: Typed arithmetic expressions (extrinsic encoding)

• Exercises 1

Class 2: Representation

• Mechanizing Metatheory in a Logical Framework discusses this material in detail.
• Exercises 2

Class 3: Mechanizing Metatheory

• Type safety for MinML (intrinsic encoding)
• Type safety for MinML (extrinsic encoding)

• Exercises 3

Additional reading

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