Garbage Collection for Higher Inductive Types
summary
Runtime integrates path-aware replacement into the normalization engine to reduce allocations by redirecting pointers to propositionally equivalent values found in an e-graph index during GC mark traversal, using two tag bits per pointer to record one of three language layers (relaxed, precise, full cubical). Prototype is implemented in cubicaltt, adds lightweight e-class insertion during execution and batch e-graph rebuilding during collection, and demonstrates faster normalization on small benchmarks (Z4 arithmetic and polynomial encodings); works as a proof‑of‑concept on GitHub but needs production GC, reclamation tuning and heap-scaling evaluation.
AI-written summary · about
chapters (17)
- 0:00Garbage collection for HITs
- 0:22Equality in cubical type theory
- 1:47HITs as quotients and efficiency
- 3:15Term optimization and memory
- 5:04Layered language design
- 7:35Runtime system and GC
- 9:20Pointer tagging for GC
- 10:01Mark phase and optimization
- 11:28E-graphs for term replacement
- 13:37Runtime summary and proof
- 14:39Future work and conclusion
- 15:01Q&A: Type preservation
- 16:15Q&A: Elaborator variations
- 16:37Q&A: Reference counting vs tracing
- 17:21Q&A: Benchmarking and egraph costs
- 18:47Q&A: Heap size impact
- 19:34Q&A: Universal algebra rewrites
related talks
14mPathological Cases for a Class of Reachability-Based Garbage Collectors
50mAn insight into Go Garbage Collection
54mGarbage Collection, State of the Art
16mSound Garbage Collection for C using Pointer Provenance
57mWriting a custom, real-world .NET GC
28mA Mechanically Verified Garbage Collector for OCaml
16mIso: Request-Private Garbage Collection
34mIt's dangerous to GC alone. Take this!