A couple more of references.

[helm.git] / helm / papers / system_T / t.tex

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 642c8c35df89c137791a0025628a4f3f540b477c..1dba53d5ba4f45c543f4ba0118f834f278e4cc88 100644 (file)
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -44,7 +44,8 @@ that the functional interpretation of the Dialectica paper
 is not among the major achievements of the author (see e.g. \cite{Girard87}), 
 the result has been extensively investigated and there is a wide 
 literature on the 
-topic (see e.g. \cite{Howard68,Troelstra,Girard87}. 
+topic (see e.g. \cite{Troelstra,HS86,Girard87}, just to mention textbooks,
+and the bibliography therein). 
 
 A different, more neglected, but for many respects much more 
 direct relation between Peano (or Heyting) Arithmetics and 
@@ -64,11 +65,12 @@ of system T, that also gives the actual computational content extracted
 from the proof. 
 In spite of the simplicity and the elegance of the proof, it is extremely
 difficult to find a modern discussion of this result; the most recent
-exposition we are aware of is in the encyclopedic (typewritten!) work by
-Troelstra \cite{Troelstra} (pp.213-229). Even modern introductory books
+exposition we are aware of is in the encyclopedic work by
+Troelstra \cite{Troelstra} (pp.213-229) going back to thirty years ago. 
+Even modern introductory books
 to Type Theory and Proof Theory devoting much space to system T
 such as \cite{GLT} and \cite{TS} surprisingly leave out this simple and 
-illuminating result. Both \cite{GLT} and \cite{TS}
+illuminating result. Both the previous textbooks
 prefer to focus on higher order arithmetics and its relation with 
 Girard's System $F$ \cite{Girard86}, but the technical complexity and
 the didactical value of the two proofs is not comparable: when you 
@@ -525,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. 
@@ -536,11 +540,15 @@ Press, 1989.
 des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
 \bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
 1990.
+\bibitem{HS86}J.R.Hindley, J. P. Seldin. Introduction to Combinators and 
+Lambda-calculus, Cambridge University Press, 1986.
 \bibitem{Howard68}W.A.Howard. Functional interpretation of bar induction
 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.