Dependently-Typed Programming with Logical Equality Reflection
summary
System DE is an explicitly typed core calculus that separates a terminating logical fragment from a potentially diverging programmatic fragment using modes for termination, lets logical proofs be reflected into typing as equality reflection so they never evaluate at runtime, and represents conversion as explicit coercion objects that are validated but erased (coercions are erasable). The metatheory—preservation, progress, and weak normalization of the logical fragment—is mechanized in a proof assistant, and the design targets elaboration into GHC Core without changing runtime behavior.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:23Dependent types matter
- 5:34Proof evaluation costs
- 10:46Partial equality problems
- 11:28System DE and modalities
- 15:19Logical equality reflection
- 18:51System DE as core calculus
- 23:51Elaboration into System DE
- 24:36Summary
- 24:57Q&A
related talks
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
52mType Theory and its Meaning Explanations
15mLogic Programming with Extensible Types (Lightning talk)
16mSyntax-Generic Operations, Reflectively Reified (Extended Abstract)
41mThe Dialectics of Type-Level Programming
46mThe Calculated Typer (Functional Pearl)
20mTowards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
52mWhat logic can teach us, Scala programmers