CMSC 32001-1: Topics in Programming Languagse (Interactive Theorem Proving)

Spring Quarter, 2006 
MWF, 11:30 am - 12:20 pm
Ryerson 276


Index

Announcements
Instructor Contact Info
Course Description
Course Textbooks
Course Policies
Course Mailing List
Running Isabelle
Slides and Demo Theories
Sample Projects
Additional Useful Links


Announcements/Updates

The first class will be on Monday, March 27, 2006 at 11:30am in Ry 276.

Instructor Contact Info

Name Role Office Office hours Phone Email
David MacQueen Professor Ryerson 152A By appointment 2-4980 dbm@cs.uchicago.edu
Robby Findler Professor Hinds 031 By appointment 2-4029 robby@cs.uchicago.edu

Course Description

This is a hands-on laboratory course in machine-assisted theorem proving using the Isabelle/HOL system. The objective is to learn the basics concepts of a typical automated logic and how to use the system to prove theorems relevant to formalizing properties of programs and languages.

Students are not expected to be familiar with mathematical logic, but previous exposure to the elementary concepts of logic and set theory and functional programming will be useful.

Course Textbook

The main textbook for the course is Isabelle/HOL: A Proof Assistant for Higher-Order Logic by Tobias Nipkow, Larry Paulson, and Markus Wenzel. This is available online as a PDF file, and may also be purchased as a paperback textbook from Amazon.

Course Mailing List

A mailing list has been created for the course. The address is cs32001@mailman.cs.uchicago.edu. The web page for the mailing list is at http://mailman.cs.uchicago.edu/mailman/listinfo/cs32001.

Isabelle

To run Isabelle on the CS network, invoke:
/stage/classes/current/32001-1/isabelle/Isabelle2005/bin/Isabelle
That should start up Emacs with ProofGeneral. You can also download and install it on your own computer from the
Isabelle web site.

Warning: This version is Isabelle2005, which is the version discussed in the printed Isabelle/HOL Tutorial. But the system available from Elsa Gunter's course web page is Isabelle2004, and the lecture slides and documentation from her web site are also for Isabelle2004. So there will be some discrepancies between the Gunter slides and demos and the printed Tutorial.

Slides and Demos

Sample Projects

Additional Useful Links


Dave MacQueen
Last modified: Wed May 17 19:59:24 CDT 2006