CS 6390: Programming Languages
MW 4:35 PM - 5:55 PM
Ford Environmental Science and Technology (EST) L1205
Prof. Bill Harris
Ms. Sulekha Kulkarni
The course will cover the formal foundations of programming language design. Examples of skills that you'll have after taking the course include:
- Proving that a program always produces a result that satisfies an expected constraint (e.g., a sorting function always returns a sorted list).
- Proving that two programs are equivalent on all inputs.
- Proving that a program transformation (e.g., a compiler optimization) always generates an equivalent program.
- Writing mathematical proofs of (simple) theorems that can be validated automatically (including all of the proofs listed above).
General topics covered will include:
- Program semantics
- Proving partial correctness properties of programs with Hoare Logic
- Program equivalence
- Lambda calculi as the foundation of functional programming
- Polymorphism and higher-order langauges
- Type systems
- Formal logic and proof systems
- Proof by induction, applied to prove properties of inductively-defined data structures (e.g., lists and trees)
The course does not have any explicit pre-requisites. However, much of the discussion will assume that students are familiar with:
- Basic notions of program representation that would be taught in an introductory course on compilers (e.g., abstract syntax).
- Basic proof techniques (e.g., induction) that would be taught in an introductory course on discrete math or logic.
Coursework will consist of:
- A set of problem sets, assigned weekly. All problems will be given as theorems to be proved in the Coq proof assistant.
- An in-class midterm and final.
The course will be based on the text Software Foundations
, which is available completely for free.
The Coq proof assistant, along with complete documentation, proof development environments, and tutorials, is also available completely for free. Software Foundations contains a sufficient explanation of Coq for all exercises that will be assigned in the course.