CS 6180

Course information provided by the Courses of Study 2017-2018.

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.

When Offered Fall.

Permission Note Enrollment limited to: graduate students.
Prerequisites/Corequisites Prerequisite: graduate standing or strong undergraduate background in programming languages or mathematical logic.

View Enrollment Information

Enrollment Information
Syllabi: none
  •  

  • 3 Credits Stdnt Opt

  • 16993CS 6180  LEC 001