From FP to OOP and Back, Consistently
summary
Extends dependent defunctionalization and refunctionalization to dependent types, proving the transformations are total and type-preserving and giving a mechanized tool that performs a one-click refactoring of data↔codata while transforming accompanying proofs. System proves type soundness but is inconsistent: it uses the Type-in-Type axiom, omits positivity checks and lacks termination/productivity checks. The talk shows three concrete failure modes — universe level annotation, negative recursive occurrences after transform, and broken termination/initialization dependencies — with working examples and an implementation artifact.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:07Object-oriented in type theory
- 2:09Data vs codata for booleans
- 3:31Refunctionalization and defunctionalization
- 5:21Dependent types and proofs
- 7:06Key contributions and soundness
- 8:30Consistency problem and vision
- 11:21Three inconsistency sources
- 12:46Universe hierarchies issues
- 13:28Positivity and binary methods
- 15:20Termination and productivity
- 17:13Project resources and closing
- 17:57Q&A
- 18:41Initialization checking question
- 20:30Answer on initialization
related talks
51mOOP v̶s̶ and FP
32mThe Evolution of Object-Oriented Programming
49mThe 4 horsemen of unsoundness in OO languages
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination
53mOOP vs FP
52mThink Abstractly, Work Concretely
18mSemantic-Type-Guided Bug Finding
34mHow I learned to stop worrying and love Functional Design