 The existence of this correspondence makes it possible to speak of a semantics of proofs, that extends to constructive formal proofs the denotational interpretations of typed \(\lambda\)-calculi, and in this context it also makes sense to ask whether an element \(x\) of some \(D^\sigma\) in a model of a typed \(\lambda\)-calculus is the interpretation of some proof of formula \(\sigma\). A further question asks whether every element of \(D^\sigma\) satisfying a suitably chosen property is the interpretation of a proof of formula \(\sigma\). Suitable properties may be for example invariance under logical relations, suitably defined over each \(D^\sigma\), like in several results of Plotkin, Statman and others summarized in Barendregt, Dekkers, &amp; Statman 2013 (I.3, I.4). We can read the latter question as asking for a strong form of completeness for that system called full completeness (Abramsky &amp; Jagadeesan 1994), whose definition can be better understood in a categorical semantics of systems of constructive logic. It is common to interpret formulas \(A\) of such systems as objects \({\lll A \rll }\) of suitable categories \(\mathbb{M}\), and proofs \(p\) of sequents \(A \vdash B\) as morphisms \(\lll p \rll : \lll A \rll \longrightarrow \lll B \rll\). While ordinary completeness states that for every valid sequent \(A \vdash B\) the set \(\mathbb{M}({\lll A \rll },{\lll B \rll })\) of morphisms is not empty, in the present setting full completeness expresses the stronger requirement that every morphism \(f: \lll A \rll \longrightarrow \lll B \rll\) in a semantical category \(\mathbb{M}\) arises as the interpretation of some proof, i.e., \(f = {\lll p \rll }\) for some proof \(p\) of the sequent \(A \vdash B\). Full completeness results have been proved for several subsystems of linear logic Girard (1987), see Abramsky (2000) for a general framework. Furthermore, it has also suggested techniques for achieving the definition of models of PCF enjoying the strong definability property required by intensional full abstraction.