The course covers topics in the theory of programming languages, types, and program verification, and how to construct and validate that theory with machine-checked proofs in the Coq proof assistant.

In this course, participants will learn about new ways of specifying, reasoning about, and developing programs and computer systems. The first half will focus on using functional programs to express and reason about computation. The second half presents methods for developing and verifying programs represented as discrete transition systems.

This seminar is an opportunity to become familiar with current research in software engineering and more generally with the methods and challenges of scientific research.