From 400e74f81d628d66e57aa4f83fd8cc299abc0506 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 3 Feb 2006 15:58:18 +0000 Subject: [PATCH] Added abstract. --- helm/papers/system_T/t.tex | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) 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} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- 2.39.2