Theory and Models of Lambda Calculus Untyped and Typed - Part 1 of 5

on YouTube ↗01h 00m

" summary

History ties Church and Curry to later work while a hands‑on session uses Mathematica rewrite rules to test combinators, demonstrating concrete reductions like SKK reduces to I and deriving a combinator for composition; an explicit variable-elimination algorithm converts lambda expressions to SKK form; the notebook demos run live and show the rewrite sequence step‑by‑step, so the claim that SNK generate all combinators is given an actual construction and working examples.

AI-written summary · about

" chapters (16)

1. 0:00Intro
2. 1:00How did I get here
3. 5:00Introduction to Mathematica
4. 7:50History of Calculus
5. 10:15Alonzo Church
6. 17:30Turing
7. 18:40Turing at Princeton
8. 20:25Griddle and El Grande
9. 26:25Can you do mathematics without variables
10. 29:10Russells paradox
11. 32:55S Combinator
12. 34:10Identity Function
13. 38:25Master Function
14. 49:25Partial Combinatorics
15. 54:35Primitive Generators
16. 55:50Variable Elimination

" related talks

• 34mAn introduction to Lambda CalculusLucas F da Costa · CityJS Conference São Paulo 2022
• 48mIt’s birds all the way down: Fun Introduction to Lambda CalculusLucas Fernandes Da Costa · Armada JS 2019
• 30mLambda Calculus: The Origins of Functional ProgrammingYassine Meherzi · Devoxx France 2021
• 21mλ-Calculus: A Brief History of Functional ProgrammingYassine Meherzi · ScalaIO 2019
• 37mLearn You Some Lambda CalculusBernardo Amorim · Code Mesh LDN 2020
• 42mPractical Lambda CalculusEinar W. Høst, Jonas Winje · Code Mesh 2015
• 40mAn Introduction to Combinator Compilers and Graph Reduction MachinesDavid Graunke · Strange Loop 2016
• 01h 34mFormal Logic UndressedPaul Snively · Scala World 2015