Quadratic type checking for objective type theory. - Benno van den Berg; Martijn den Besten (CoRR, 2021)