CS 6860 Fall 15:
10:10AM - 11:25AM
Since the previous offering of this course there have been many significant developments in the topics covered. Some advances are related to major successes in using proof assistants to formally reason about programs and software systems, including compilers, operating systems, and distributed systems. Some are discoveries about the logics implemented by the proof assistants.
This course will examine one or two of these successes as case studies.
This offering does not assume knowledge about formal methods or proof assistants. It assumes background in logic at the college level, e.g. as taught in CS2800 or Math/CS 4860.
The course will cover elements of the Coq and Nuprl proof assistants and discuss new proof assistants being built, such as Idris and F* at MSR. Coq and Nuprl use constructive logic, so that topic will also be covered from the start, and teaching constructive logic will be a review of basic logic. Topics include results about uniform validity that led to a constructive completeness proof for intuitionistic first-order logic with respect to its evidence semantics. Evidence semantics will be developed for classical logics, including HOL (Higher-Order Logic, used by the family of HOL proof assistants).
Open problems will be discussed, some concerning the logical foundations, some concerning the challenges of specifying and verifying software. Grading will be based on individual projects designed by the student and on a two or three problem sets.
Members of the PRL research group will assist with aspects of the course such as demonstrating and teaching about proof assistants.
320 Gates Hall
Office Hours: After class and by appointment
Time: Tues/Thurs 10:10AM - 11:25AM
Location: Upson 215