From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 10 Nov 2005 12:13:53 +0000 (+0000)
Subject: A couple more of references.
X-Git-Tag: V_0_7_2_3~95
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=178c7763dd83a9c2e463a3593e6e6c9177a5cb39;p=helm.git

A couple more of references.
---

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 614037caa..1dba53d5b 100644
--- 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.