From: Andrea Asperti <andrea.asperti@unibo.it>
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}