CS 430/530 Schedule, Spring 2025
Course Schedule
CS430/530: Formal Semantics, Spring 2025, Yale University
Last modified: November 8, 2024. This page is still under construction.
1/14:
Lecture: Introduction
1/16:
Lecture: Math Background; Predicate Logic (Reynolds Appendix and 1)
1/21:
Lecture: Coq Basics; Inductive Definitions (SF
Basics
and
Preface
; Harper 1-2)
1/23:
Lecture: Induction in Coq (SF
Induction
and
Lists
)
1/28:
Lecture: Imp; Denotational Semantics (Reynolds 2)
1/30:
Lecture: Denotational Semantics; Failures (Reynolds 2 and 5)
Assignment 1
Due
2/4:
Lecture: Full Abstraction; Input-Output and Continuations (Reynolds 2 and 5)
2/6:
Lecture: Operational Semantics (Reynolds 6)
Assignment 2
Due
2/11:
Lecture: More about Coq (SF
Poly
and
MoreCoq
)
2/13:
Lecture: Axiomatic Semantics; Hoare Logic (Reynolds 3)
2/14:
Lecture: Inductive Predicates ( SF
Prop
and
MoreProp
)
2/18:
Lecture: Logic in Coq; Imp in Coq (SF
Logic
and
Imp
and
Equiv
)
Assignment 3
Due
2/20:
Lecture: Hoare Logic in Coq; Judgments (SF
Hoare
; Harper 2-3)
2/25:
Lecture: Static & Dynamic Semantics; Type Safety (Harper 4-7)
2/27:
Lecture: Function Types; System T; PCF (Harper 8-10)
3/4:
Lecture: Finite Data Types (Harper 11-14)
Assignment 4
Due
3/6:
Lecture: Smallstep, Auto, Simply Typed Lambad Calculus in Coq (SF
Smallstep
,
Auto
,
Types
, and
Stlc
)
3/25:
Lecture: Finite and Infinite Data Types (Harper 11-16)
3/27:
Lecture: Lambda Calculus; Dynamic Types (Harper 17-19)
4/1:
Lecture: Polymorphism and Abstract Types (Harper 20-21)
Assignment 5
Due
4/3:
Lecture: Control Stacks; Exceptions (Harper 27-28)
4/8:
Lecture: Continuations; Curry-Howard Correspondence (Harper 29-30)
4/10:
Lecture: Types and Propositions (Harper 30-31)
Assignment 6
Due (extended)
4/15:
Lecture: Case Study (Certified OS Kernels)
4/17:
Lecture: Case Study (Certified Compilers)
4/22:
Lecture: TBA
4/24:
Lecture: Summary and Reviews
Assignment 7
Due
5/1:
Final Project
Due
Copyright (c) 2013,
Zhong Shao
, Dept. of
Computer Science
,
Yale University
