@misc{indiciae226abeddaba9, title = {Complete Bidirectional Typing for the Calculus of Inductive Constructions}, author = {Meven Lennon-Bertrand}, year = {2021}, url = {https://arxiv.org/abs/2102.06513}, note = {Source identifier: 2102.06513} }