Lecture Notes
CS430/530: Formal Semantics, Fall 2013, Yale University
Lecture notes will be made shortly after each lecture.
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
The following are the lecture notes used in Fall 2011:
Lectures 1-2
(Aug 31 - Sep 5):
Introduction; Predicate Logic
(
notes
)
Lectures 2-3
(Sep 5 - 12):
Inductive Definitions and Judgments
(
pdf
)
Lectures 4-5
(Sep 14 - 19):
Imp; Denotational Semantics
(
pdf
)
Lecture 6
(Sep 21):
Failure, Input-Output, and Continuations
(
pdf
)
Lecture 7
(Sep 26):
Operational Semantics
(
pdf
)
Lecture 8
(Sep 28):
Axiomatic Semantics
(
pdf
)
Lecture 9
(Oct 3):
Static & Dynamic Semantics; Type Safety
(
pdf
)
Lecture 10
(Oct 5):
Function Types; System T; PCF
(
pdf
)
Lecture 11
(Oct 10):
Finite Data Types
(
pdf
)
Lecture 12
(Oct 12):
Infinite Data Types
(
pdf
)
Lecture 13
(Oct 17):
Lambda Calculus; Dynamic Types
(
pdf
)
Lectures 14-15
(Oct 19-24):
Variable Types
(
pdf
)
Lecture 16
(Oct 26):
Control Effects
(
pdf
)
Lecture 17
(Oct 31):
Separation Logic; Assertions
(Reynolds
Course Notes 1-2
)
Lecture 18
(Nov 2):
Separation Logic Specifications
(Reynolds
Course Notes 3
)
Lecture 19
(Nov 7):
Lists and List Segments
(Reynolds
Course Notes 4
)
Lecture 20
(Nov 9):
Types and Propositions
(
pdf
Lecture 21
(Nov 14):
Storage Effects
(
pdf
)
Lecture 22
(Nov 16):
Shared-Variable Concurrency
(
pdf
)
Lecture 23
(Nov 28):
Process Calculus; Concurrency
(
pdf
)
Lecture 24
(Nov 30):
Equational Reasoning; Parametricity
(
pdf
)
Copyright (c) 2013
Zhong Shao
, Dept. of
Computer Science
,
Yale University