CS 430/530 Schedule, Fall 2011
Course Schedule
CS430/530: Formal Semantics, Fall 2013, Yale University
Last modified: October 3, 2013. This page is still under construction.
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
