History and Philosophy
 Philosophy of Computer Science (Draft text)
 History of Lambda Calculus and Combinatory Logic
 A Profile of Mathematical Logic (A fun, quickish read on the story of modern logic)
 The Search for Mathematical Roots, 18701940: Logics, Set Theories and the Foundations of Mathematics from Cantor through Russell to Gödel (A grownup text on much of the same.)
 The history of the theory of computation
 DeBruijn and Automath: the first proof checker
Proofs and Theory
 Why we study proofs
 Starting with a Theory of Computation course
 Teaching theory of computation through search
 Keeping logic in the trivium of computer science: a teaching perspective
 Dr. Spencer’s Mantra for the relief of anxiety that accompanies attempts to prove theorems
Just Good Fun
 Logicomix (It’s a comic about Russell and early 20th century mathematical logic. ᕕ( ᐛ )ᕗ)
 SKI Combinator Tetris
 Care for your pet combinator
CS and CS Inspired Fiction
 “The Thrilling Adventures of Lovelace and Babbage”
 Chiang’s short story “Seventytwo Letters” (Audio version)
 Chiang’s “Division by Zero” (a story about exfalso quodlibet)

Russell’s “The Metaphysician’s Nightmare” (a story about the troubles with negation).
 Automatically generating /conjectures/
PL and More
 The first recursive but not primitiverecursive function
 Pattern matching coming to Python
 Hutton’s Tutorial on
fold
operators  On Barron & Strachey’s Cartesian product function
 The feeling you should get looking at a self interpreter
 Reynold’s “Definitional Interpreters for Higherorder Programming Languages” (Updated Notes)
 Norman on “Denotational Design” (sort of our style of writing interpreters)
 Danvy & Nielsen’s “Defunctionalization at Work”
 Essay: “What does valof defunctionalize?”
 Vanier’s blogpost on the Y combinator
 Yin Wang’s slide deck on (re)deriving the Y combinator
 The smallest (in AIT) fixpoint combinator
 Polyvariadic fixpoint combinators for mutual recursion
 Hunting the history of Moses Schönfinkel
 Kleene’s “Church predecessor” via a trip to the dentist
 QuineMcCluskey Algorithm, Visualized
 Someone else’s explanation of the CPS transformation
 A firstorder onepass CPS transformation
 Why continuations are coming to Java
 Lambda: the Ultimate GOTO
 CONS should not cons its arguments pt II: Cheney on the MTA
 (An operational investigation of) the CPS Hierarchy
 Church encoding is the vistor pattern
 BohmBerarducci encoding–an extension of Church encoding
Relational and Logic Programming
 miniKanren.org
 van Emden on relational programming, logic beyond prolog
 Purity and programming purely in Prolog
 Paulson on logic programs as inductive definitions
PL Course notes I can recommend
 PPL Notes
 Krishnamurthi’s PLAI
 Barzilay’s PL class notes
 An agda based introduction to PL