Eliminating reflection from type theory
Abstract
International audience
DOI 10.1145/3293880.3294095
Related papers
- Dependent Ghosts Have a Reflection for Free ICFP 2024
- Bounded Sort Polymorphism with Elimination Constraints POPL 2026
- Mechanizing Synthetic Tait Computability in Istari CPP 2026
- Toward foundations for type-reflective metaprogramming GPCE 2009
- ANF preserves dependent types up to extensional equality JFP 2022
- Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism ECOOP 2023
- The fire triangle: how to mix substitution, dependent elimination, and effects POPL 2020
- From Semantics to Syntax: A Type Theory for Comprehension Categories POPL 2026