Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau: Eliminating reflection from type theory. CPP 2019: 91-103