From d10018fb879fe85d595750903a7e168372bba257 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 10 Nov 2005 08:46:30 +0000 Subject: [PATCH] Extended bibliography. --- helm/papers/system_T/t.tex | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) 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. -- 2.39.2