The Curry-Howard correspondence connects the simply typed calculus with proofs in propositional intuitionistic logic. This correspondence can be extended between System F (polymorphic typed calculus) and proofs in first-order logic.
I've been wondering what would be the logical/type-theoretical counterpart of a dependent system like the calculus of constructions. The wiki article says
The Calculus of Constructions can be considered an extension of the Curry–Howard isomorphism. [...] The Calculus of Constructions extends this isomorphism to proofs in the full intuitionistic predicate calculus, [...]
I'm not sure what "the full intuitionistic predicate calculus" means (no internal link or citation provided there, plus I'm looking for a type theory, not a calculus) but, judging from what I read in the article about intuitionistic type theory, my intuition sees a correspondence that smells Curry-Howardy. Is there, though, some (more formal) discussion on this?