## Course Schedule## CS430/530: Formal Semantics, Fall 2013, Yale University |

- 8/28:
- Lecture: Introduction
- 8/30:
- Lecture: Math Background; Predicate Logic (Reynolds Appendix and 1)

- 9/4:
- Lecture: Coq Basics; Inductive Definitions (SF Basics and Preface; Harper 1-2)

- 9/9:
- Lecture: Induction in Coq (SF Induction and Lists)
- Section on Coq (7:30-9pm, Room 307 AKW)
- 9/11:
- Lecture: Imp; Denotational Semantics (Reynolds 2)
- 9/13:
- Section on Coq (11:30am-1pm, Room 307 AKW)

- 9/16:
- Lecture: Denotational Semantics; Failures (Reynolds 2 and 5)
**Assignment 1**Due- 9/18:
- Lecture: Full Abstraction; Input-Output and Continuations (Reynolds 2 and 5)

- 9/23:
- Lecture: Operational Semantics (Reynolds 6)
- 9/25:
- No Lecture
**Assignment 2**Due

- 9/30:
- Lecture: More about Coq (SF Poly and MoreCoq)
- 10/2:
- Lecture: Axiomatic Semantics; Hoare Logic (Reynolds 3)
- 10/4:
- Lecture: Inductive Predicates ( SF Prop and MoreProp)

- 10/7:
- Lecture: Logic in Coq; Imp in Coq (SF Logic and Imp and Equiv)
**Assignment 3**Due- 10/9:
- Lecture: Hoare Logic in Coq; Judgments (SF Hoare; Harper 2-3)

- 10/14:
- Lecture: Static & Dynamic Semantics; Type Safety (Harper 4-7)
- 10/16:
- Lecture: Function Types; System T; PCF (Harper 8-10)

- 10/21:
- Lecture: Finite Data Types (Harper 11-14)
**Assignment 4**Due- 10/23:
- FALL RECESS

- 10/28:
- Lecture: Smallstep, Auto, Simply Typed Lambad Calculus in Coq (SF Smallstep, Auto, Types, and Stlc)
- 10/30:
- Lecture: Finite and Infinite Data Types (Harper 11-16)

- 11/4:
- Lecture: Lambda Calculus; Dynamic Types (Harper 17-19)
- 11/6:
- Lecture: Polymorphism and Abstract Types (Harper 20-21)
**Assignment 5**Due

- 11/11:
- Lecture: Control Stacks; Exceptions (Harper 27-28)
- 11/13:
- Lecture: Continuations; Curry-Howard Correspondence (Harper 29-30)

- 11/18:
- Lecture: Types and Propositions (Harper 30-31)
**Assignment 6**Due (extended)- 11/20:
- Lecture: Case Study (Certified OS Kernels)
- 11/21:
**Assignment 6**Due

- 11/25:
- THANKSGIVING RECESS
- 11/27:
- THANKSGIVING RECESS

- 12/2:
- Lecture: Case Study (Certified Compilers)
- 12/4:
- Lecture: Summary and Reviews
**Assignment 7**Due

- 12/11:
**Final Project**Due

Copyright (c) 2013, Zhong Shao, Dept. of Computer Science, Yale University