Consistency of a Dependent Calculus of Indistinguishability
summary
Defines a concrete instance DCOIω with an infinite predicative universe hierarchy and proves logical consistency, strong normalization, and that type conversion is decidable. Proofs are fully mechanized in Coq mechanization and the paper ships reusable artifacts (artifact evaluation badge). Semantics account for observer-indexed indistinguishability, dependency contexts, and erased indices; the work extracts a normalization-based decision procedure and demonstrates no closed term inhabits False under the given axioms.
AI-written summary · about
chapters (12)
- 0:00Decoy introduction and goals
- 1:06Type soundness in decoy
- 2:10Decoy omega as logic
- 3:56Dependency tracking
- 5:19Dependency levels in types
- 7:04Indistinguishability for proof irrelevance
- 9:08Runtime eraser with type indices
- 11:37Logical consistency via predicates
- 13:44Indistinguishability in semantics
- 15:32Meta-theoretic properties
- 16:13Related work and conclusion
- 16:39Q&A