A couple more of references.

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 614037caafb97c75a526dc255511e724222c7be0..1dba53d5ba4f45c543f4ba0118f834f278e4cc88 100644 (file)
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -527,6 +527,8 @@ Q(c_i~\vec{m}~\vec{t})$.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{thebibliography}{}
+\bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures. 
+Foundations of Computing, Cambrdidge University press, 1991.
 \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. 
@@ -545,6 +547,8 @@ by bar recursion. Compositio Mathematica 20, pp.107-124. 1958
 \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{Kleene45}S.C.Kleene. On the interpretation of intuitionistic 
+number theory. Journal of Symbolic Logic, n.10, pp.109-124, 1945.
 \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.