A Formalization of Opaque Definitions for a Dependent Type Theory
summary
Formal development of top-level opaque definitions is mechanized in Agda and proves that adding opacity preserves subject reduction, normalization, consistency and decidable conversion; the system models definitions as a definition context with names, types and definients and implements per-definition unfolding vectors plus a transparentization operator that enforces transitive unfolding. The paper builds the extension atop a graded dependent type theory, gives typing and delta rules that block or allow unfolding, and the mechanization and proofs succeed.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 2:31Problems with unfolding
- 3:58Opacity controls unfolding
- 4:39Formalizing opaque definitions
- 7:05Definition contexts
- 9:11Augmenting definitions
- 13:02Well-formedness with opacity
- 14:30Normalization via logical relations
- 16:37Summary
- 17:30Q&A
- 18:13Top-level opacity limits
- 20:54Parameterized modules
- 21:57Observational indistinguishability
- 22:42Q&A and closing
related talks
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
25mShallowly embedding type theories
19mDeriving Dependently-Typed OOP from First Principles
16mA Hoare-Logic Style Refinement Types Formalisation
30mNormalisation for First-Class Universe Levels
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
52mType Theory and its Meaning Explanations
23mImpredicative Observational Equality