From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 3 Feb 2006 15:58:18 +0000 (+0000)
Subject: Added abstract.
X-Git-Tag: make_still_working~7642
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=400e74f81d628d66e57aa4f83fd8cc299abc0506;p=helm.git

Added abstract.
---

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index a3f08cd5a..20ec95149 100644
--- 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}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%