CMSC631: Program Analysis and Understanding

Spring, 2019

This course introduces the concept of formal verification with applications to programming language theory. It revolves around the idea that both mathematical statements and computer programs can be treated as objects of computation and mathematically checked by a computer. We will study this area in some depth, using the Coq proof assistant to formalize core concepts in mathematics, logic, type theory and programming languages theory.