CADE Tutorial
Mechanizing Metatheory with LF and STELF
Section titled “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 June 10, 2013, 9:00-12:30, co-located with CADE 2013, in Lake Placid, New York. Location “Mirror Lake” in The Crowne Plaza Resort.
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.
The tutorial is organized and jointly presented by the the IT University of Copenhagen and the CMU Principles of Programming group. The presenters and TAs at CADE will be Taus Brock-Nannestad, Chris Martens, and Carsten Schürmann.
Schedule
Section titled “Schedule”The tutorial will begin at 9:00AM. Get [http://www.demtech.dk/raw-attachment/wiki/News/lectures.pdf the slides]!
- Part 1: Basic STELF Skills
- Part 2: Mechanizing MinML
- Part 3: Combinators: Worlds and Adequacy
- Coda: What’s next?
There will be a coffee break at 10:30AM.
Get STELF before the tutorial!
Section titled “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: see the download page.
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.)
Sponsors
Section titled “Sponsors”Thanks to our sponsors: [http://www.cs.cmu.edu Carnegie Mellon School of Computer Science], [http://www.demtech.dk DemTech Project], [http://www.itu.dk IT University of Copenhagen],