- Schedule of Classes - January 7, 2018 7:14PM EST
- Course Catalog - January 7, 2018 7:15PM EST
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.
Credits and Grading Basis
3 Credits Stdnt Opt(Letter or S/U grades)
Class Number & Section Details
- TRPhillips Hall 403
Or send this URL: