Theory & Models of Lambda Calculus: Typed and Untyped (Part 6)
summary
Claims a concrete model: using the powerset of the integers with enumeration operators to model application, abstraction and computability, then adds a topology so types inherit computational and topological structure. Builds dependent types as Pi and Sigma as dependent types and constructs recursive dependent functions with the Y combinator, investigates polymorphism via the pair combinator polymorphism and Church numerals, and uses complete-lattice fixed-point theorems to explain least/greatest fixed points and where arrow fails monotonicity.
AI-written summary · about
chapters (5)
- 0:00Start
- 2:26Two Zeros Function
- 4:58Generalizing to Sums
- 14:45Function Space
- 26:13Polymorphism with Type Constructors
related talks
01h 12mTruth about Types
45mPractical Lambda Calculus
41mWar Time Proofs and Futuristic Programs
01h 20mA Practical Introduction to Haskell GADTs
01h 52mIsomorphic Reasoning: Counting with Types Part 3
57mPropositions as Types
43mPropositions as Types
06mDistribution Theoretic Semantics for Non-Smooth Differentiable Programming