Theory & Models of Lambda Calculus: Typed and Untyped (Part 1)
summary
Shows a concrete model: application and abstraction realized by enumeration operators on P(N) with a topology, not handwavy category talk. Carries out variable-elimination into combinators, builds Church numerals and a fixed-point combinator for recursion, and demonstrates primitive and nonprimitive recursion constructions. Explains how types emerge as quotients of subspaces inside the model and gives the actual combinators and constructions used so the model can be checked or reimplemented.
AI-written summary · about
chapters (7)
- 0:00Start
- 8:02History of Lambda Calculus
- 20:43What Lambda Calculus
- 40:31Lambda Postfix Notation
- 42:25Category Theory Is Type Theory
- 44:57Successor Function
- 55:39Fixed Point Combinator
related talks
45mPractical Lambda Calculus
01h 12mTruth about Types
41mWar Time Proofs and Futuristic Programs
01h 52mIsomorphic Reasoning: Counting with Types Part 3
01h 20mA Practical Introduction to Haskell GADTs
01h 01mCategory Theory - Part 2 of 6
02h 28mIsomorphic Reasoning: Counting with Types Part 2
01h 39mIsomorphic Reasoning: Counting with Types Part 1