Added abstract.

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index a3f08cd5a66fd43832cfa49f469e0381817ab280..20ec951492223efb55f63fa2aec8ddf9eb2329ee 100644 (file)
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -43,7 +43,19 @@
 \thispagestyle{empty}
 
 \begin{abstract}
-...
+In 1959, Kreisel introduced a notion of ``modified'' realizability to
+provide an alternative technique to G\"odel functional (dialectica)
+interpretation for establishing the connection between Peano Arihtmetic
+and System T. While the dialectica interpretation has been widely
+studied in the literature, Kreisel's technique, although remarkably 
+simpler,has apparently been almost neglected (with the only exception
+of Troelstra). In this paper we give a modern presentation of the technique, 
+and generalize it to arbitrary inductive types in a first order setting.
+This is part of a larger program, advocating the study 
+of logical systems with primitive inductive types starting form
+weak, predicative logical frameworks and adding little by little small 
+bits of logical power.
+
 \end{abstract}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%