I am trying to understand how the type theory of the COQ theorem prover (calculus of constructions or CIC) works. Wikipedia states that it can be considered an extension of the Curry-Howard isomorphism.
For constructive propositional logic the Curry-Howard isomorphism states that types can be seen as propositions, and proofs as programs. For types/propositions $A,B$, propositions can be viewed as types in the following way (propositions on the left, types on the right, $\Leftrightarrow$ denoting correspondence)
$$A\rightarrow B \Leftrightarrow A\Rightarrow B$$ $$A\land B \Leftrightarrow A\times B$$ $$A\lor B\Leftrightarrow A+B$$
Then, for example, proving that
$$\forall A\forall B: A\rightarrow A\lor B,$$ where $A,B$ are interpreted as types can be seen as a proof that for any types $A,B$, the type $A\Rightarrow A+B$ exists. Proof of this fact can be converted into program and vice versa. In this case the program would simply return an $x\in A$, e.g. the left side of the pair, thereby showing the type exists.
Ok, so now to the question. CIC implements a predicate logic. How are the terms $\forall x: A.B$, $\lambda x: A.B$ interpreted in the correspondence? An example would be fine. Keep in mind I am very new to this $\lambda$ notation.