Objective
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)
Resources
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.