Instructor:
Konstantinos Mamouras
Class meetings:
Tuesdays and Thursdays at 2:30 pm - 3:45 pm at Duncan Hall 1046
Office hours:
Mondays 10:00 am - 11:00 am at Duncan Hall 3081
Teaching assistant: Zhiwei Zhang (office Duncan Hall 3060)
Office hours:Wednesdays 5:30 pm - 6:30 pm at Duncan Hall 3110
The grade will be based on the homeworks (50%), two takehome midterms (15% and 15% respectively), and one takehome final (20%).
The homeworks and the exams should be submitted on time. For late homeworks there will be a 25% penalty for each day of delay. Late exam submissions will not receive any credit.
| Date | Topic | Readings |
|---|---|---|
| January 8 | Introduction, Programming in Coq | Preface, Basics |
| January 10 | Proof by Induction | Induction |
| January 15 | NO CLASS | |
| January 17 | Tutorial: Programming in Coq & Induction | Basics, Induction |
| January 22 | Working with Structured Data | Lists |
| January 24 | Polymorphism & higher-order functions | Poly |
| January 29 | Polymorphism & higher-order functions | Poly |
| January 31 | Tactics in Coq | Tactics |
| February 5 | Logic in Coq | Logic |
| February 7 | NO CLASS | |
| February 12 | Logic in Coq | Logic |
| February 14 | Inductively Defined Propositions | IndProp |
| February 19 | Inductively Defined Propositions | IndProp |
| February 21 | Inductively Defined Propositions | IndProp |
| February 26 | Total and Partial Maps | Maps |
| February 28 | Review | |
| March 5 | The Curry-Howard Correspondence | ProofObjects |
| March 7 | Induction Principles | IndPrinciples |
| March 12 | NO CLASS | |
| March 14 | NO CLASS | |
| March 19 | Simple Imperative Programs | Imp, ImpParser, ImpCEvalFun |
| March 21 | Program Equivalence | Equiv |
| March 26 | Hoare Logic, Part I | Hoare |
| March 28 | Hoare Logic, Part II | Hoare2, HoareAsLogic |
| April 2 | Small-step Operational Semantics | Smallstep |
| April 4 | SMT-based Verification and Synthesis, Part I | |
| April 9 | SMT-based Verification and Synthesis, Part II | |
| April 11 | Type Systems | Types |
| April 16 | The Simply Typed Lambda-Calculus (STLC) | Stlc |
| April 18 | Properties of the STLC | StlcProp |
If a student misses a course meeting, they are expected to review the corresponding material on their own.
In this course, all students will be held to the standards of the Rice Honor Code, a code that you pledged to honor when you matriculated at this institution. If you are unfamiliar with the details of this code and how it is administered, you should consult the Honor System Handbook. This handbook outlines the University's expectations for the integrity of your academic work, the procedures for resolving alleged violations of those expectations, and the rights and responsibilities of students and faculty members throughout the process.
If you have a documented disability or other condition that may affect academic performance you should: 1) make sure this documentation is on file with Disability Support Services (Allen Center, Room 111 / adarice@rice.edu / x5841) to determine the accommodations you need; and 2) talk with the instructor to discuss your accommodation needs.