Deriving Dependently-Typed OOP from First Principles
summary
Derives a dependently typed object-oriented fragment by duality and gives a concrete calculus with two symmetric language fragments plus type- and semantics-preserving defunctionalization and refunctionalization transformations. Implements the system in Rust with an LSP/VSCode extension and WebAssembly examples, can transform a full 500-line proof of simply-typed lambda calculus soundness by a click, and proves the transformations total and inverse (modulo alpha when no local matches). System is sound but intentionally inconsistent: no termination/positivity checks and restricted judgmental equalities.
AI-written summary · about
chapters (8)
- 0:00Dependently-typed OOP intro
- 1:08Functional vs OO booleans
- 3:36Refunctionalization & defunctionalization
- 5:42Dependent types & correctness proofs
- 7:31User-defined types including functions
- 11:24System achievements & limits
- 14:12Implementation & demos
- 15:20Q&A
related talks
42mDOT: Scala Types from Theory to Practice
18mDeveloping a Dependently Typed Language with Runtime Proof Search
15mStable Relations and Abstract Interpretation of Higher-Order Programs
01h 07mBuilding a Dependently Typed Language in Haskell Part 1
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
19mCombining Dependency, Grades, and Adjoint Logic
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
19mExtensible Metatheory Mechanization via Family Polymorphism