Toggle navigation
Home
Links
Event-b
B-method page
Idris-lang
Hillel Wayne: Formal Methods
Kozen's notes
Exercises
Partial and Total orders
Formulas for Sets
Slides
Introduction and Set Theory
Notebooks
Languageofsets.ipynb
Notes
About Notes
Dependent Type theory
Inductive types and type families
These are David Kozen's programming language course notes, downloaded about a decade ago.
Lecture 1: Introduction
Lecture 2: Lambda Calculus
Lecture 3: Equivalence, Reductions and Normal Forms
Lecture 4: λ Encodings and Recursion
Lecture 5: IMP: Big-Step and Small-Step Semantics
Lecture 6: Well Founded Induction
Lecture 7: Inductive Definitions and the Knaster–Tarski Theorem
Lecture 8: Evaluation Contexts
Lecture 9: Semantics via Translation
Lecture 10: Types and Scope Rules
Lecture 11: Computing with Closures
Lecture 12: Modules and State
Lecture 13: Predicate Transformers
Lecture 14: Axiomatics Semantics II and Hoare Logic