POPL Tutorial/Saturday

Notes from Saturday

Please fill out our _[https://spreadsheets.google.com/viewform?key=p0-89EvFXQhUXF827jjk_Dg feedback form]_.

If you have questions, you can email a TA at twelfelf@gmail.com.

Check out Session 5’s material: do some practice problems, email us feedback.

Mechanizing Metatheory with LF and STELF

Do you want to learn how to use STELF to specify, implement, and prove properties about programming languages?

Come to the STELF tutorial on January 19, 2009, co-located with POPL 2009, in Savannah, Georgia.

Learn to:

• Represent languages and logics in LF
• Prove metatheorems with STELF under the helpful guidance of STELF experts.

The tutorial will be a highly interactive introduction to LF and STELF aimed at programming languages researchers. No prior experience with LF and STELF is presumed. Participants will leave the workshop with experience in reading and writing LF representations of programming languages, and experience reading, writing, and debugging STELF proofs.

Register at the [http://www.regmaster.com/conf/popl2009.html POPL 2009 registration site]!
The early registration deadline is December 19.

The tutorial is organized and presented by the CMU Principles of Programming group.

Schedule

• Session 1 (11AM-noon): [http://www.cs.cmu.edu/~drl/tmp/twelflectures.pdf Overview of LF and STELF]
• Session 2 (12:15-1:15PM): Working with STELF
• Session 3 (1:30PM-2:30PM): [http://www.cs.cmu.edu/~drl/tmp/twelflectures.pdf Adequacy]
• Pizza break
• Session 4 (3:00PM-4:30PM): Type safety for MinML
• Session 5 (4:45PM-6:15PM): Work on exercies

Get STELF before the tutorial!

The tutorial will be interactive, with participants writing STELF code, so you should come with STELF installed on your laptop.

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