From: Andrea Asperti Date: Mon, 17 Oct 2005 07:47:53 +0000 (+0000) Subject: Added basic bibliography. X-Git-Tag: V_0_7_2_3~212 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb5c410736244f89736ea8f63a570f1db4db8d75;p=helm.git Added basic bibliography. --- diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index db212276d..2c7e420a8 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -233,6 +233,38 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. \end{itemize} \begin{thebibliography}{} +\bibitem{GLT}G.Y.Girard. Proof Theory and Logical Complexity. +Bibliopolis, Napoli, 1987. +\bibitem{GLT}G.Y.Girard, Y.Lafont, P.Tailor. Proofs and Types. +Cambridge Tracts in Theoretical Computer Science 7.Cambridge University +Press, 1989. +\bibitem{God}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung +des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958. +\bibitem{God}K.G\"odel. Collected Works. Vol.II, Oxford University Press, +1990. +\bibitem{How}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{Let}P.Letouzey. Programmation fonctionnelle certifi\'ee; l'extraction +de programmes dans l'assistant Coq. Ph.D. Thesis, Universit\'e de +Paris XI-Orsay, 2004. +\bibitem{Loef}P.Martin-L\"of. Intuitionistic Type Theory. +Bibliopolis, Napoli, 1984. +\bibitem{Pau87}C.Paulin-Mohring. Extraction de programme dans le Calcul de +Constructions. Ph.D. Thesis, Universit\'e de +Paris 7, 1987. +\bibitem{Pau89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs from proofs +in the Calculus of Constructions. In proc. of the Sixteenth Annual +ACM Symposium on +Principles of Programming Languages, Austin, January, ACML Press 1989. +\bibitem{Sch}K.Sch\"utte. Proof Theory. Grundlehren der mathematischen +Wissenschaften 225, Springer Verlag, Berlin, 1977. +\bibitem{Tro}A.S.Troelstra. Metamathemtical Investigation of Intuitionistic +Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer Verlag, +Berlin, 1973. +\bibitem{TS}A.S.Troelstra, H.Schwichtenberg. Basic Proof Theory. +Cambridge Tracts in Theoretical Computer Science 43.Cambridge University +Press, 1996. \end{thebibliography}