then using the constants $c_X$ of type $\neg\neg X \f X$. With such a translation the type does not change.

Since the translation of a term of the form $\m\a.M$ uses the type of $\a$, a formal presentation of this translation would need the use of $\l$-calculus and $\l\m$-calculus\
à la Church. For simplicity of notations we have kept a presentation à la Curry, mentioning the types only when it is necessary.

We extend the system ${\cal S}$ by adding, for each propositional variable $X$, a constant $c_X$. When the constants that occur in a term $M$ are $c_{X_1},...,c_{X_n}$, the notation $\G \v_{{\cal
S}^c} M : A$ will mean $\G,c_{X_1}:\neg \neg X_1 \f
X_1,...,c_{X_n}:\neg \neg X_n \f X_n \v_{{\cal S}} M : A$.

For every $A \in {\cal T}$, we define a $\l$-term $T_A$ as follows:

-   $T_{\bot} = \l x. (x \; \l y.y)$

-   $T_X = c_X$

-   $T_{A \f B} = \l x.\l y. (T_B \; \l u.(x \; \l v. (u \; (v \;
    y))))$

\[tran\] For every $A \in {\cal T}$, $\v_{{\cal S}^c} T_A : \neg \neg A \f A$.

By induction on $A$.

1.  We associate to each $\m$-variable $\a$ of type ${\neg A}$ 