Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach
summary
Shows that reduce-and-compare becomes decidable again with surjective pairing by restricting transitivity to a syntactically defined SN good set of strongly normalizing terms, proving termination by a minimal logical-relation argument, and proving confluence only on SN terms. Reduction-based algorithm is proven sound and complete relative to a typed expansion algorithm; development is fully mechanized in Rocq mechanization and totals about 10,000 LOC, with the confluence portion ≈2–3k lines and reusable artifacts available.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 2:04Algorithmic conversion in type theory
- 6:39Subjective pairing challenges
- 9:57Typed vs untyped equality
- 13:15Soundness in typed reduction
- 15:43Strongly normalizing terms
- 17:31Syntactic approach and implementation
- 19:16Conclusion and future work
- 20:45Q&A
related talks
28mFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
29mUnification Modulo Isomorphisms between Dependent Types for Type-based Library Search
31mCertification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
23mNormalizable types
14mA dependently typed calculus with pattern matching and erasure inference
56mOn Type-Based Techniques for Program Manipulation
29mA Term Matching Algorithm and Substitution Generality