# Curry-Howard correspondence in CIC/propositional logic?

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.

$$\forall x: A.B$$ is a type. It is interpreted as a terminating algorithm that takes in an $$A$$ and produces a $$B$$ as a result.
$$\lambda x: A. M$$ is a function. It takes an input $$x$$ of type $$A$$ and returns $$M$$ (which might reference $$x$$).
Under the Curry-Howard correspondence this is interpreted as a proof of $$A$$ implies $$B$$ (when $$M$$ has type $$B$$)..