Say you wrote a function `reverse` that takes a list and reverses it, so e.g. `reverse [1,2,3]` becomes `[3,2,1]`. Clearly, this function, if implemented correctly, has the property that applying it twice in succession on a list returns the same list. In a conventional programming language, you could write a few unit tests that verify this property holds for a few examples; but you cannot prove the property in general by covering all cases, since there are infinitely many. Coq, however, is not a conventional programming language...

This course introduces basic concepts and techniques in the foundational study of programming languages, stressing their formal logical underpinnings. The central theme is the view of individual programs and programming languages as mathematical objects about which precise claims may be made and proven. The whole course will be taught using the Coq proof assistant, a popular interactive theorem prover implementing a dependently typed functional programming language. Particular topics include operational techniques for formal definition of language features, type systems and type safety properties, polymorphism and subtyping, and Hoare logic. If time permits, we will also study the formal verification of fundamental data structures implementations.

Prior knowledge of Coq or functional programming is not required. Since Coq has a steep learning curve, the course will require considerable time and effort, including weekly homework and self-learning of some material that will not be covered in lectures and tutorials.

The main texts for the course are the online books available at [https://softwarefoundations.cis.upenn.edu].