From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 10 Nov 2005 08:46:30 +0000 (+0000)
Subject: Extended bibliography.
X-Git-Tag: V_0_7_2_3~99
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d10018fb879fe85d595750903a7e168372bba257;p=helm.git

Extended bibliography.
---

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 642c8c35d..614037caa 100644
--- 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 
@@ -536,6 +538,8 @@ 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.