CS 6390: Programming Languages

Time	MW 4:35 PM - 5:55 PM
Location	Ford Environmental Science and Technology (EST) L1205
Instructor	Prof. Bill Harris (KACB 2322)
Teaching Assistant	Ms. Sulekha Kulkarni

Navigation

• Objective
• Pre-requisites
• Structure
• Resources

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)

Pre-requisites

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.

Structure

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.

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.