Logic, Programs & Verification

• Term: Spring 2025
• Time: Thursday 6:30pm – 9:20pm
• Place: Falmouth Hall, Room 313 (North Campus)
• Intructor: Paul Downen <paul@pauldownen.com>
• Office: Dandeneau Hall, Room 305
• Office Hours: Tue 2:30pm – 4:00pm, Wed 2:00pm – 3:30pm, or by appointment

Have you ever been frustrated after spending hours trying to debug a program, but didn't know what the problem was?

Have you struggled with putting together a proof for a theory class, but didn't know what needs to be said, how it is supposed to come together, or if you made some obscure mistake?

Do you wish your computer could help you fix these problems, instead of causing more of them?

Logic, Programs & Verification is about the proofs-as-programs paradigm, where you can learn the tools that can give you confidence that your programs do what you want, as well as instructing your computer to make mathematical proofs for you. By the end of the semester, you will know how to use formal methods to specify what programs should do, implement software based on that specification, and verify that your code is correct.

This course will include an introduction to different systems of formal logic and their connection to programming languages. We will use the relationship between proofs and programs to describe the desired behavior of code in a way a computer can understand, and use formal methods to write machine-checked proofs of correctness.

On the practical side, this course will offer hands-on experience with software tools known as proof assistants — specifically Coq — to write programs and proofs at the same time. For exercises, we will use the textbook Software Foundations that provides both working examples and practice problems. Students will have time to work on these exercises and get feedback and assistance from the instructor during an in-class lab session (in the second half of the posted class time) following lecture.

At the end of this course, students should be

• • able to understand and create formal statements about mathematical theorems or specifications of program behavior,
• • proficient in using the Coq proof assistant for writing and checking proofs of formal theorems,
• • knowledgeable in the correspondence between statically typed computer progrrams and formal mathematical proofs,
• • comfortable in the meaning and writing of informal, "pen-and-paper" proofs.

Prerequisite: Department approval

Suggested prerequisite: Discrete Math, Organization of Programming Languages, Functional Programming, Design of Programming Languages, or equivalent.

Students should have some comfortable with basic "pen-and-paper" proofs as seen in classes like Discrete Math or Organization of Programming languages. write significant programs in some language. Previous experience with some functional programming (OCaml, Haskell, Scheme, F#, Scala, Clojure, ...) is a plus, but not necessary.