Course Schedule
CS430/530: Formal Semantics, Spring 2025, Yale University
Last modified: March 29, 2025. This page is still under construction.
- 1/14:
- Lecture: Introduction
- 1/16:
- Lecture: Math Background; Predicate Logic (Reynolds Appendix and 1)
- 1/21:
- Lecture: Inductive Definitions; Coq Basics (Harper 1-2; SF
Basics and
Preface)
- 1/23:
- Lecture: Induction in Coq (SF
Induction
and Lists);
- 1/28:
- Lecture: Imp; Denotational Semantics (Reynolds 2)
- 1/30:
- Lecture: Denotational Semantics (Reynolds 2)
- Assignment 1 Due
- 2/4:
- Lecture: Full Abstraction; Failures and Input-Output (Reynolds 2 and 5)
- 2/6:
- Lecture: Input-Output and Continuations; Operational Semantics (Reynolds 5 and 6)
- Assignment 2 Due
- 2/11:
- Lecture: More about Coq (SF
Poly
and Tactics)
-
- 2/13:
- Lecture: Operational Semantics; Axiomatic Semantics (Reynolds 6 and 3)
- 2/18:
- Lecture: Axiomatic Semantics; Hoare Logic (Reynolds 3)
- 2/20:
- Lecture: Logic in Coq; Inductive Predicates (
SF Logic
and IndProp)
- Assignment 3 Due
- 2/25:
- Lecture: Imp in Coq; More Automation
(SF Maps
and Imp
and Auto
)
- 2/27:
- Lecture: Hoare Logic in Coq
(SF Equiv
and Hoare
and Hoare2);
Judgments and Rules (Harper 1-3)
- 3/4:
- Lecture: Static & Dynamic Semantics; Type Safety (Harper 4-7);
Smallstep in Coq (SF Smallstep)
- 3/6:
- Lecture: Total Functions; Finite Data Types (Harper 8-11);
STLC in Coq (Types,
Stlc,
and StlcProp)
- Assignment 4 Due
- 3/25:
- Lecture: Infinite Data Types (Harper 14-15)
- 3/27:
- Lecture: Polymorphism and Abstract Types (Harper 16-18)
- 4/1:
- Lecture: Recursive Functions and Types (Harper 19-20);
- Assignment 5 Due
- 4/3:
- Lecture: Control Stacks; Exceptions; Continuations (Harper 28-30)
- 4/8:
- Lecture: Game Semantics
- 4/10:
- Lecture: Lambda Calculus; Dynamic Types (Harper 21-23)
- Assignment 6 Due
- 4/15:
- Lecture: Symbols; Mutable State (Harper 31-32, 34-35)
- 4/17:
- Lecture: Lazy Evaluation; Parallelism (Harper 36-38)
- 4/22:
- Lecture: Dynamic Classification; Concurrency (Harper 33, 39-40)
- Assignment 7 Due
- 4/24:
- Lecture: Real-World Formal Methods
- 5/7:
- Final Project Due
Copyright (c) 2025,
Zhong Shao,
Dept. of
Computer Science,
Yale University