The Implicit Calculus of Constructions as a Programming Language with Dependent Types