CS 430/530 Schedule, Spring 2025
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: Concurrency and Distribution (Harper 39-41)
Assignment 7
Due
4/24:
Lecture: Equational Reasoning (Harper 46-48)
5/1:
Final Project
Due
Copyright (c) 2025,
Zhong Shao
, Dept. of
Computer Science
,
Yale University
