Formal Methods Foundation

Course Description

This is an advanced graduate course on formal method foundations. The primary goal of this course is to provide students with an understanding of the basic concepts of formal methods, and their applications in computer science. Roughly, there are six board topics will be covered:

• Constructive logic: propositional, first-order, and second order
• Dependent type theory: theory and its applications
• Proof theory: including (semi-)automatic theorem proving and practical proof engineering
• Functional programming: especially the connection with logic via Curry-Howard isomorphism
• Operational semantics
• Type systems

Prerequisite: basic discrete mathmatics. Some familarity with functional programming is better, but not required.