- Instructor of Record: Prof. Christian Skalka
- 3 credits
- Weekly seminar on Tuesdays 2:45-4:15, Innovation E325
This course is a seminar-style independent study group focused on automated proof assistants and mechanized metatheory. We will specifically focus on Coq and EasyCrypt. We will investigate both foundational elements of these systems, but our focus will be on practical use. We will mainly consider applications to functional and stateful programming languages as well as probabilistic programming especially for cryptographic protocols.
After completing this study the student will be able to:
- Understand how pen-and-paper logic principles are converted to code in proof assistants.
- Understand how to use proof assistants for defining and proving properties of programs, including:
- Both functional and stateful programs.
- Defining and reasoning about inductive structures.
- Probabilistic programming- how and why.
- Write verified proofs of simple functional programs in Coq
- Write verified proofs of simple probabilistic programs in EasyCrypt
- Understand and prove probabilistic noninterference of simple programs in EasyCrypt.
- maybe we will learn about Polaris, which is similar to EasyCrypt but is in Coq and incorporates concurrency.
All materials are freely available online. Our main text for initial exploration of Coq is Software Foundations. We will also use EasyCrypt- this has an associated paywalled tutorial text that will not be strictly necessary but you can optionally purchase for reference.
You will also need access to working implementations of Coq and EasyCrypt, and an IDE such as Proof General in Emacs is strongly recommended.
We will use this Git repo for managing and sharing code. We will maintain a resources.md file in the repo with links to relevant resources for the course. We have a Team for this course, that you should be a member of if enrolled, that we will use for course-related communications.
This is an advanced graduate-level seminar course and students will be expected to be highly engaged and self-motivated. Our focus will be on exploring and learning challenging material together. Students are expected to attend all seminars, and each week a different class participant will be responsible for leading discussion of the next topic of study. Student performance evaluation will be based on engagement and quality of in-class presentations, including proofs.
https://www.uvm.edu/policies/student/acadintegrity.pdf
As a faculty member, I want you to get the most you can out of this course. You play a crucial role in your education and in your readiness to learn and fully engage with the course material. It is important to note that alcohol and cannabis can seriously impair your ability to learn and retain information up to 48 hours or more after use.
In keeping with University policy, any student with a documented disability interested in utilizing accommodations should contact SAS, the office of Disability Services on campus. SAS works with students and faculty in an interactive process to explore reasonable and appropriate accommodations, which are communicated to faculty in an accommodation letter. All students are strongly encouraged to meet with their faculty to discuss the accommodations they plan to use in each course. A student's accommodation letter lists those accommodations that will not be implemented until the student meets with their faculty to create a plan. Contact SAS: A170 Living/Learning Center; 802-656-7753; access@uvm.edu; or www.uvm.edu/access
Students have the right to practice the religion of their choice. Each semester students should submit in writing to their instructors by the end of the second full week of classes their documented religious holiday schedule for the semester. An arrangement can then be made to make up the missed work.
In order to be excused from classes, student athletes should submit appropriate documentation to the Professor in advance of all scheduling conflicts within the first two weeks of class. Those missing class are expected to submit make-up assignments within a reasonable time period.