%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thebibliography}{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thebibliography}{}
\bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
years later. Theoretical Computer Science 45, 1986.
\bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity.
\bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
years later. Theoretical Computer Science 45, 1986.
\bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity.
\bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions.
in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory
Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
\bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions.
in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory
Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
\bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of
constructive functionals of finite type. In. A.Heyting ed.
{\em Constructivity in mathematics}. North Holland, Amsterdam,1959.
\bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of
constructive functionals of finite type. In. A.Heyting ed.
{\em Constructivity in mathematics}. North Holland, Amsterdam,1959.