Theory and Models of Lambda Calculus Untyped and Typed - Part 5 of 5
summary
Shows how untyped lambda over PERs and the power set of N with Scott topology produce models of dependent and polymorphic type theory, giving a local cartesian closed category of quotients. Demonstrates concrete constructions: Church numerals, addition/multiplication via composition, a predecessor via pair trick, and encoding of products, sums and function-space isomorphisms. Argues continuity forces intuitionistic logic and that lattice intersections yield polymorphism; treats proofs as explicit lambda programs.
AI-written summary · about
chapters (6)
- 0:00Start
- 1:00Disjoint Sum of Two Partial Equivalence Relations
- 5:07Dependent Types
- 5:44Dependent Products in Dependent Type Theory
- 10:18Polymorphism of Type
- 23:13Conclusion
related talks
41mWar Time Proofs and Futuristic Programs
04mSeparated and Shared Effects in Higher-Order Languages
01h 04mThe Leibniz Library and Applied Propositions as Types
39mA Little Taste of Dependent Types
41mInfinite Lambda Calculus
44mSome History of Functional Programming Languages
01h 00mProspects for Computer Formalization of Infinite-Dimensional Category Theory
06mLightning Talk: The Lambda Calculus in C++ Lambdas