History and Philosophy

• Philosophy of Computer Science (Draft text)
• History of Lambda Calculus and Combinatory Logic
• A Profile of Mathematical Logic (A fun, quick-ish read on the story of modern logic)
• The Search for Mathematical Roots, 1870-1940: Logics, Set Theories and the Foundations of Mathematics from Cantor through Russell to Gödel (A grown-up 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 “Seventy-two Letters” (Audio version)
• Chiang’s “Division by Zero” (a story about ex-falso 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 primitive-recursive 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 Higher-order 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) fix-point combinator
• Poly-variadic fixpoint combinators for mutual recursion
• Hunting the history of Moses Schönfinkel
• Kleene’s “Church predecessor” via a trip to the dentist
• Quine-McCluskey Algorithm, Visualized
• Someone else’s explanation of the CPS transformation
• A first-order one-pass 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
• Bohm-Berarducci 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