Instructor:
Konstantinos Mamouras
Class meetings:
Mondays, Wednesdays and Fridays 9:45 am - 10:40 am (online)
Office hours:
Tuesdays 11:00 am - 12:00 pm (online)
Teaching assistant:
Zhifu Wang
Office hours:
Thursdays 11:00 am - 12:00 pm (online)
The grade will be based on homework assignments (70%) and a final project (30%).
Date | Topic | Readings |
---|---|---|
January 25 | Introduction, Functional Programming | Preface, Basics |
January 27 | Functional Programming | Basics |
January 29 | Functional Programming | Basics, Induction |
February 1 | Functional Programming | Induction |
February 3 | Functional Programming | Lists |
February 5 | Functional Programming | Polymorphism |
February 8 | Logic | Logic in Coq |
February 10 | Constructive Interpretation of Logic | Logic in Coq |
February 12 | Inductively Defined Propositions | IndProp |
February 15 | CLASS CANCELED due to storm | |
February 17 | NO CLASS | |
February 19 | CLASS CANCELED due to storm | |
February 22 | Reasoning about Relations | Relations |
February 24 | More about Relations | Relations |
February 26 | Imperative Programming | Winskel, Chapter 2 |
March 1 | NO CLASS | |
March 3 | Operational Semantics | Winskel, Chapter 2 |
March 5 | The Logic of Partial Correctness | Winskel, Chapter 6 |
March 8 | The Logic of Partial Correctness | Winskel, Chapter 6 |
March 10 | The Logic of Partial Correctness | Dafny |
March 12 | The Logic of Partial Correctness | Dafny |
March 15 | Propositional Logic | BM, Chapter 1 |
March 17 | Propositional Satisfiability | BM, Chapter 1 |
March 19 | Propositional Satisfiability | BM, Chapter 1 |
March 22 | First-Order Logic, Syntax | BM, Chapter 2 |
March 24 | First-Order Logic, Semantics | BM, Chapter 2 |
March 26 | NO CLASS | |
March 29 | First-Order Logic, Sequent Calculus | BM, Chapter 2 |
March 31 | First-Order Theories, Quantified Linear Arithmetic | BM, Chapters 3 and 7 |
April 2 | Quantified Linear Arithmetic, Quantifier Elimination | BM, Chapter 7 |
April 5 | Quantified Linear Arithmetic, Quantifier Elimination | BM, Chapter 7 |
April 7 | Theory of Equality | BM, Chapter 9 |
April 9 | Theory of Equality | BM, Chapter 9 |
April 12 | Reasoning about Arrays | BM, Chapter 9 |
April 14 | Nelson-Oppen Combination Method | BM, Chapter 10 |
April 16 | Nelson-Oppen Combination Method | BM, Chapter 10 |
April 19 | Nelson-Oppen Combination Method | BM, Chapter 10 |
April 21 | The Z3 Theorem Prover | Z3 Tutorial |
April 23 | Static Analysis | NNH, Chapter 2 |
April 26 | Static Analysis | NNH, Chapter 2 |
April 28 | Abstract Interpretation | NNH, Chapter 4 |
April 30 | Course Conclusion | Notes on Canvas |
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.