Teaching

Part IA

1. 1Representations · Abstraction Barriers · Floating-Point Imprecision · Functional Programming Basics · Recursion and Iteration · Efficiency · Lists
2. 2More on Lists · Sorting · Trees · Datatypes
3. 3Datatypes · Dictionaries and Functional Arrays · Functions as Values · Sequences and Laziness
4. 4Sequences and Laziness · Queues and Search Strategies

Part IB

1. 1Syntax and Semantics · Small-Step Operational Semantics · Types · Inductive Definitions · Inductive Proof · L1 Metatheory
2. 2Function Basics · Functions in L2 · L2 Metatheory · Products, Sums and Curry–Howard · Mutable References and Store Typing
3. 3Evaluation Contexts · Exceptions · Subtyping · Concurrency · Contextual Equivalence

Part IB

1. 1Computability · Algorithmically Undecidable Problems · Register Machines · Gödel Encoding · Universal Register Machine
2. 2The Halting Problem and Decidability · Turing Machines · Primitive Recursive Functions · The Lambda Calculus: Syntax · The Lambda Calculus: Equational Systems
3. 3The Lambda Calculus: Normal Forms · Lambda-Definable Functions