Lecture Notes
CS430/530: Formal Semantics, Spring 2025, Yale University
Lecture notes will be made shortly after each lecture.
Lectures 1-2
(Jan 14 - 16):
Introduction; Predicate Logic
(
notes
)
Lectures 3-4
(Jan 21 - 23):
Inductive Definitions
; (
pdf
)
Coq Tutorial
(
Basics
,
Induction
, and
Lists
)
Lectures 5-6
(Jan 28 - 30):
Imp; Denotational Semantics
(
pdf
)
The following are the lecture notes used in Fall 2013:
Lectures 1-2
(Aug 28 - 30):
Introduction; Predicate Logic
(
notes
)
Lectures 3-5
(Sep 4 - 11):
Inductive Definitions
(
pdf
);
Coq Tutorial
(
Basics
,
Induction
, and
Lists
)
Lectures 5-6
(Sep 11 - 16):
Imp; Denotational Semantics
(
pdf
)
Lectures 6-8
(Sep 16 - 23):
Failure, Input-Output, and Continuations
(
pdf
)
Lectures 9-10
(Sep 23 - 30):
Operational Semantics
(
pdf
)
Lectures 10-12
(Sep 30 - Oct 4):
Axiomatic Semantics
(
pdf
);
More Coq
(
Poly
,
MoreCoq
,
Prop
,
MoreProp
)
Lectures 13-15
(Oct 7 - 14):
Logic & Imp in Coq
(
Logic
,
Imp
,
Equiv
,
Hoare
)
Lecture 16
(Oct 16):
Static & Dynamic Semantics; Type Safety
(
pdf
)
Lecture 17
(Oct 21):
Function Types; System T; PCF
(
pdf
)
Lecture 18
(Oct 28):
Smallstep, Auto, and Simply Typed Lambda Calculus in Coq
(
Smallstep
,
Auto
,
Types
, and
Stlc
)
Lecture 19
(Oct 30):
Finite and Infinite Data Types
(
pdf
and
pdf
)
Lecture 20
(Nov 4):
Lambda Calculus; Dynamic Types
(
pdf
)
Lecture 21
(Nov 6):
Polymorphic and Abstract Types
(
pdf
)
Lectures 22-23
(Nov 11-13):
Control Effects
(
pdf
)
Lectures 23-24
(Nov 13-18):
Types and Propositions
(
pdf
)
Lecture 25
(Nov 20):
Certified OS Kernels
Copyright (c) 2025
Zhong Shao
, Dept. of
Computer Science
,
Yale University
