COMP 360C
Spring 2026
| Section:
01
|
There is a strong correspondence between mathematics and programming, under which mathematical proofs correspond to programs. A _proof assistant_ is a tool that a mathematician/programmer can use to represent proofs/programs, in such a way that a computer can verify whether or not they are correct. The use of proof assistants in math and computer science is becoming ever more important for managing the increasing complexity of proofs and programs. Proof assistants have been used to check significant mathematical theorems, such as the Four Color Theorem and the Feit-Thompson Odd-Order Theorem, as well as large pieces of software, such as a C compiler and the definition of the Standard ML programming language. In this course, students will learn to use the Agda proof assistant to write computer-checked programs and proofs. |
|
| Credit: 1 |
Gen Ed Area Dept:
NSM MATH |
| Course Format: Lecture | Grading Mode: Graded |
| Level: UGRD |
Prerequisites: COMP212 AND MATH228 |
|
Fulfills a Requirement for: None |
|
Past Enrollment Probability: 90% or above |
| SECTION 01 |
| Instructor(s): Licata,Dan Times: ..T.R.. 02:50PM-04:10PM; Location: OLIN014; |
| Total Enrollment Limit: 25 | | SR major: 15 | JR major: 10 | | |
| Seats Available: 8 | GRAD: X | SR non-major: 0 | JR non-major: 0 | SO: 0 | FR: 0 |
| Drop/Add Enrollment Requests | | | | | |
| Total Submitted Requests: 0 | 1st Ranked: 0 | 2nd Ranked: 0 | 3rd Ranked: 0 | 4th Ranked: 0 | Unranked: 0 |
|