From 178c7763dd83a9c2e463a3593e6e6c9177a5cb39 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 10 Nov 2005 12:13:53 +0000 Subject: [PATCH 1/1] A couple more of references. --- helm/papers/system_T/t.tex | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index 614037caa..1dba53d5b 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -527,6 +527,8 @@ Q(c_i~\vec{m}~\vec{t})$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{thebibliography}{} +\bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures. +Foundations of Computing, Cambrdidge University press, 1991. \bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen years later. Theoretical Computer Science 45, 1986. \bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity. @@ -545,6 +547,8 @@ by bar recursion. Compositio Mathematica 20, pp.107-124. 1958 \bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions. in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory Logic, Lambda calculus and Formalism. Acedemic Press, 1980. +\bibitem{Kleene45}S.C.Kleene. On the interpretation of intuitionistic +number theory. Journal of Symbolic Logic, n.10, pp.109-124, 1945. \bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of constructive functionals of finite type. In. A.Heyting ed. {\em Constructivity in mathematics}. North Holland, Amsterdam,1959. -- 2.39.2