COMP 408/548 - Verified Programming

Instructor: Konstantinos Mamouras
Class meetings: Tuesdays and Thursdays at 2:30pm-3:45pm at Duncan Hall 1046
Office hours: Mondays 10:00am-11:00am at Duncan Hall 3081

Teaching assistant: Zhiwei Zhang (office Duncan Hall 3060)
Office hours:Wednesdays 5:30pm-6:30pm at Duncan Hall 3110

Course Description

The course will explore the mathematical underpinnings of reliable software. The students will learn how to use the interactive proof assistant Coq to construct software along with a machine-checkable proof of its correctness. Basic concepts of logic, functional programming, static type systems and deductive verification will be covered.

Required Texts and Materials

We will use the books Logical Foundations and Programming Language Foundations of the Software Foundations series.

Grade Policies

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.

Course Schedule

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

Absence Policies

If a student misses a course meeting, they are expected to review the corresponding material on their own.

Rice Honor Code

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.

Disability Support Services

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 / / x5841) to determine the accommodations you need; and 2) talk with the instructor to discuss your accommodation needs.