Lawson Computer Science Building
The goal of this course is the study of programming languages from a foundational viewpoint. We will examine the design, implementation and theory of programming languages features. We will give particular emphasis on aspects of reliability, both of the language and of programs written using the language. To that end, we will develop and use tools that enable reasoning about both the design and specification of new language features, and that allow precise understanding of the rationale for existing features in modern languages. This course will not be a survey of existing languages or language features. Instead, we will explore ways to understand programming languages generally that help us to answer questions such as the following:
To help answer these questions, the course is designed around several interleaved themes: (1) the role of logic and proofs in programming language design; (2) formal reasoning devices (aka operational and axiomatic semantics) that precisely explain the meaning of programming language features and program executions; (3) the use of types to define and specify safety conditions on program executions, and to enrich language expressivity; (4) the use of automated proof assistants to help validate important theorems that describe useful properties based on the structure of (2) and (3), using techniques enabled by (1).
At the end of this class, students should be comfortable with modern notions of language semantics and specification, have developed sufficient mathematical maturity to formally prove interesting properties about a language features, type systems, or complex computation structures generally, and be capable of understanding current research trends in the field.
The course will be divided into roughly four parts:
It is assumed that students taking this class would have had some exposure to an undergraduate programming languages class (equivalent to CS 465), and are comfortable with basic mathematical concepts (e.g., graph and set theory).
There will be assignments given every week. These assignments will take the form of programming exercises in Coq; most of these exercises will entail developing mechanized proofs whose correctness is automatically checked by Coq. Thus, These exercises will require students to define various concepts, and prove important theorems about the topics discussed during the lecture, using Coq. Students are encouraged to work together on these assignments.
There will be a semester-long project that will involve using Coq to define a formal system of a computing artifact (e.g., a type system, a concurrency abstraction, a security policy, etc.), develop theorems and proofs about existing systems, explore program analysis definitions and correctness, etc. Students can work teams or individually. A proposal indicating the project topic, justification, and methodology must be submitted and approved by (TBD). Projects will be due at the end of the semester.
The course is structured around the following book by Benjamin Pierce:
Useful supplemental material can also be found in
In addition, students might also find the following texts useful:
There are a number of tutorials and detailed documentation available on Coq:
Copies of the lectures and handouts will be available through the course
The course will leverage piazza (http://piazza.com), an interactive Q&A newsgroup messaging system that allows students, faculty, and TAs to post questions (and answers) to problems and issues related to the course.
The course will roughly follow the breakdown given below.
|Polymorphism and Higher-Order Programming|
|Propositions, Evidence, and Relations|
|Program Semantics||Imperative Programs|
|Hoare Logic and Axiomatic Semantics|
|Types||Simply-Typed Lambda Calculus|
|Typing Judgments, Contexts, and Relations|
|More on Types||Existential Types|