CS 6115CS 6115 - Certified Software Systems
This course provides a hands-on introduction to programming and verification using the Coq proof assistant.
- Coordinates
- 10:10am – 11:25am Tuesday & Thursday in Phillips Hall 407
- Instructors
-
- Nate Foster (jnfoster@cs.cornell.edu)
Office Hours: Wednesday 1:30-2:30pm (Gates 432) - Jules Jacobs (jj758@cornell.edu)
Office Hours: Any time by appointment (Gates 430)
- Nate Foster (jnfoster@cs.cornell.edu)
Schedule
| Date | Topic | Lectures | Homework |
|---|---|---|---|
| Week 1: Introduction to Coq | |||
| Tue 08/27 | Course overview | [ slides | web | coq ] | |
| Thu 08/29 | Propositional Reasoning | [ slides | web | coq ] | HW1 goes out |
| Week 2: Data Types, Induction, and Modules | |||
| Tue 09/03 | Natural numbers | [ slides | web | coq ] | |
| Thu 09/05 | Lists and Modules | [ slides | web | coq ] | HW1 is due; HW2 goes out |
| Week 3: Interpreters, Inductive Relations | |||
| Tue 09/10 | Interpreters | [ slides | web | coq ] | |
| Thu 09/12 | Inductive Relations | [ slides | web | coq ] | |
| Week 4: Semantics (Big-Step, Small-Step) | |||
| Tue 09/17 | Big-Step Semantics | [ slides | web | coq ] | |
| Thu 09/19 | Small-Step Semantics | [ slides | web | coq ] | HW2 is due; HW3 goes out |
| Week 5: Advanced Coq (Fuel, Type Classes, Automation) | |||
| Tue 09/24 | Foundations, Fuel, and Type Classes | [ slides | web | coq ] | |
| Thu 09/26 | Type Classes and Auto-mation | [ slides | web | coq ] | |
| Week 6: Lambda Calculus, Types | |||
| Tue 10/01 | Progress and Preservation | [ slides | web | coq ] | |
| Thu 10/03 | Termination | [ slides | web | coq ] | HW3 is due; HW4 goes out |
| Week 7: Hoare Logic | |||
| Tue 10/08 | Shallow Embedding | [ slides | web | coq ] | |
| Thu 10/10 | Separation Logic | [ slides | web | coq ] | |
| Week 8: More Separation Logic | |||
| Tue 10/15 | No class: Fall Break | ||
| Thu 10/17 | Concurrent Separation Logic | [ slides ] | HW4 and Project Proposal are Due |
| Week 9: Reflection | |||
| Tue 10/22 | Simple Reflection | [ slides | web | coq ] | |
| Thu 10/24 | More Reflection | [ slides | web | coq ] | |
| Week 10: Dependent Types | |||
| Tue 10/29 | Dependent Types | [ slides | web | coq ] | |
| Thu 10/31 | More Dependent Types | [ slides | web | coq ] | |
| Week 11: More Dependent Types | |||
| Tue 11/05 | Even More Dependent Types | [ slides | web | coq ] | |
| Thu 11/07 | Implementing Dependent Type Theory | [ slides ] | |
| Week 12: Coinduction | |||
| Tue 11/12 | Introduction to Coinduction | [ slides | web | coq ] | |
| Thu 11/14 | Coinduction in Coq | [ slides | web | coq ] | |
| Week 13: Regular Expressions | |||
| Tue 11/19 | Derivatives | [ web | coq ] | Project Check-In Due |
| Thu 11/21 | Parsing | [ slides ] | |
| Week 14: Victory Lap | |||
| Tue 11/26 | Victory Lap | [ slides | web | coq ] | |
| Thu 11/28 | No class: Thanksgiving | ||
| Week 15: Project Presentations | |||
| Tue 12/03 | |||
| Thu 12/05 | |||
| Final Project | |||
| Mon 12/16 | No class | Final Project Due @ 4:30pm | |
Guidelines
Method of Assessing Student Achievement
Grades for the course will be calculated as follows:
- Participation: 10%
- Homework: 40%
- Final Project: 40%
- Presentation: 10%
This course uses a letter grading system, which is the official grading system at Cornell University. Typically, 80-90% of the students in this course receive a grade of A- or higher and the median grade is typically an A.
Academic Integrity
Absolute integrity is expected of all Cornell students in every academic undertaking. The course staff will prosecute violations aggressively using automatic detection tools.
You are responsible for understanding every word of these policies:
- Cornell University Code of Academic Integrity
- Computer Science Department Code of Academic Integrity
Under no circumstances may you hand in work done with or by someone else under your own name or share code with anyone else unless explicitly allowed. If you are unsure about what is permissible and what is not, please ask!
Special Needs and Wellness
It is Cornell policy to provide reasonable accommodations to students who have a documented disability (e.g., physical, learning, psychiatric, vision, hearing, or systemic) that may affect their ability to participate in course activities or to meet course requirements. Students with disabilities are encouraged to contact Student Disability Services at 607-254-4545, or the instructor for a confidential discussion of their individual needs.
If you are experiencing undue personal or academic stress at any time during the semester or need to talk to someone who can help, contact the instructor or:
- Engineering Academic Advising at 607-255-7414,
- Learning Strategies Center at 607-255-6310,
- Let’s Talk Drop-in Counseling at Gannett at 607-255-5155
- Empathy Assistance and Referral Service at 607-255-EARS.
Resources
Software Setup
Students will need to install the Coq proof assistant itself, as well as an integrated development environment.- For installing Coq, we recommend using opam.
- There are several options for IDEs including:
- ProofGeneral: an Emacs-based IDE,
- VSCoq: a Visual Studio Code extension for Coq
- JSCoq: a web-based IDE, or
- CoqIDE: a standalone, graphical IDE
And if you run into any trouble, please don't hesitate to contact the course staff. We would be very glad to help.