Bruno Bernardo. Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable. (An implicit Calculus of Constructions with dependent sums and decidable type inference). PhD thesis, École Polytechnique, Palaiseau, France, 2015. [doi]
Abstract is missing.