CS 6180

Last Updated

  • Schedule of Classes - January 7, 2018 7:14PM EST
  • Course Catalog - January 7, 2018 7:15PM EST

CS 6180
Introduction to Constructive Type Theory

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

Syllabi: none

  •   Regular Academic Session. 

  • 3 Credits Stdnt Opt

  • 16993 CS 6180   LEC 001

  •