Summer school 2008

NOTOC This page contains course materials for the STELF course at [http://www.cs.uoregon.edu/research/summerschool/summer08/ 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 STELF.

New: Feedback Form

Please fill out our [http://gs4080.sp.cs.cmu.edu/servlets/summerschool2008/feedback.ss feedback form]!

Get STELF

Pre-built binaries of STELF are available for most operating systems through the [http://twelf.plparty.org/builds STELF Night(ly)].

• [http://twelf.plparty.org/builds/twelf-linux.tar.gz Linux (tgz)]
• [http://twelf.plparty.org/builds/twelf.exe Windows (exe)]
• [http://twelf.plparty.org/builds/twelf-osx-intel.dmg Mac OS 10.4 or 10.5 (Intel only) (dmg)]

Otherwise:

• you can build STELF from the [http://twelf.plparty.org/builds/twelf-src.tar.gz source tarball]. You will need [http://www.mlton.org MLton] or [http://www.smlnj.org 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 STELF with Emacs for the basics of interacting with STELF. (You can also use STELF without Emacs, by interacting with the STELF server directly.)

Lectures and Labs [http://www.cs.cmu.edu/~rwh/talks/UO_Summer08.pdf (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

• [http://www.cs.cmu.edu/~drl/pubs/hl07mechanizing/hl07mechanizing.pdf 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 [http://www.cs.cmu.edu/~rwh/plbook/book.pdf Practical Foundations for Programming Languages] as a reference for basic PL concepts.
• MMLF: [http://www.cs.cmu.edu/~drl/pubs/hl07mechanizing/hl07mechanizing.pdf Mechanizing Metatheory in a Logical Framework] discusses LF, representation, and mechanized metatheory in technical detail.
• Proving metatheorems with STELF is a self-contained intro tutorial on this wiki.
• After you get spun up, there are lots of tutorials and case studies.