When Does a Program Typecheck?
summary
Formalizes when an expression typechecks by writing down simply typed lambda calculus syntax, typing judgments and the three concrete rules: variable, abstraction and application; extends with built-in naturals and shows the proof tree that the identity applied to 0 types as int; gives small-step semantics and proves progress and preservation to establish type soundness, so a specification plus semantic reductions — not an implementation — guarantees well behaved execution.
AI-written summary · about
chapters (9)
- 0:00Intro
- 0:51In a statically typed language
- 1:46Type systems are not arbitrary
- 2:34Formalizing type systems
- 3:21Simply-typed lambda calculus
- 5:34Example
- 6:59Type soundness
- 8:09Conclusion
- 8:53Questions?
related talks
22mA Certifying Proof Assistant for Synthetic Mathematics in Lean
01h 08mLean: Machine-Checked Mathematics and Verified Programming, Past and Future
35mProof Theory Impressionism: Blurring the Curry-Howard Line
01h 04mThe Leibniz Library and Applied Propositions as Types
01h 44mAn Introduction to Natural Deduction
41mWar Time Proofs and Futuristic Programs
32mSafer Code with LLMs: Scala Types Silver Bullet?
01h 00mAI Safety through Programming?