CS 6180

Introduction to Constructive Type Theory

Course Description

Course information provided by the 2017-2018 Catalog.

Constructive type theory is the mathematical foundation for modern proof assistants, which are software systems used to help verify the correctness of programs and mathematical proofs. Proof assistants are also used in teaching advanced programming and are essential tools in the study of formal methods. This course will cover the basics of the theory and then explore a number of applications ranging from verification that programs correctly meet their stated specifications to their use in solving open problems in mathematics. The extensive and rich research literature over the past forty years, along with several textbooks, will form the basis of this course.

Prerequisites/Corequisites Prerequisite: graduate standing or strong undergraduate background in programming languages or mathematical logic.

Permission Note Enrollment limited to: graduate students.

When Offered Fall.

View Enrollment Information