The Troll in Your Machine — A Brief Introduction to the Thought of Jean-Yves Girard
summary
Overview of Jean-Yves Girard’s contributions: the system F (polymorphic lambda calculus), linear logic, and the Girard paradox. Shows links between Girard’s work and modern languages (Rust’s ownership typing from linear logic, Haskell/Scala generics from system F) and gives a concrete encoding: a session-typed client/server where a client sends two ints and a server returns their sum, using linear negation to represent protocol duality.
AI-written summary · about
chapters (12)
- 0:00Presentation of Jean-Rémy Girard
- 1:29Science makes us know all the things that exist
- 2:18The Logis cistes
- 4:56Semantics
- 5:46Realist semantics
- 8:28The 3 basements
- 9:26Basements in logic
- 10:02System F
- 10:37Inheritances
- 12:59Negation
- 13:40Reintroducing the subject into logic
- 14:08Conclusion
related talks
56mThe Tale of Troy
37mA (Not So Gentle) Introduction To Systems Programming In ATS
57mOo Considered Harmful
01h 01mValue Semantics: Safety, Independence, Projection, & Future of Programming
47mKilled by Worse is Better What we can learn from the last time FP failed (TBR)
49mThe Eternal Sunshine of the Spotless Programming Language
30mDebugging Trait Errors as Logic Programs
44mTyped Design Patterns for the Functional Era