|
|
Dec 11, 2024
|
|
CS 6180 - Introduction to Constructive Type Theory Fall. 3 credits. Student option grading.
Prerequisite: strong undergraduate background in programming languages or mathematical logic. Permission of instructor required. Enrollment limited to: graduate students.
Staff.
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.
Add to Favorites (opens a new window)
|
|
|