Bibliografia

[APSSa]

Asperti A., Padovani L., Sacerdoti Coen C., and Schena I. Content Centric Logical Environments. Short Presentation at LICS 2000.

[APSSb]

Asperti A., Padovani L., Sacerdoti Coen C., and Schena I. Formal Mathematics in MathML. To be presented at MathML International Conference 2000.

[APSSc]

Asperti A., Padovani L., Sacerdoti Coen C., and Schena I. Towards a Library of Formal Mathematics. Accepted at TPHTOOLS 2000.

[APSSd]

Asperti A., Padovani L., Sacerdoti Coen C., and Schena I. XML, Stylesheets and the re-mathematization of formal content. Submitted to LPAR 2000.

[Bar92]

Barendregt H. Lambda Calculi with Types. In Abramsky, Samson and others, editor, Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1992.

[BBC⁺97]

Barras B., Boutin S., Cornes C., Courant J., Filliatre J. C., Giménez E., Herbelin H., Huet G., Munoz C., Murthy C., Parent C., Paulin-Mohring C., Saibi A., and Werner B. The Coq Proof Assistant Reference Manual : Version 6.1. Technical Report RT-0203, Inria (Institut National de Recherche en Informatique et en Automatique), France, 1997.

[Ber89]

Berners-Lee T. Information Management: A Proposal. 1989.

[BW97]

Barras B. and Werner B. Coq in Coq. Submitted, 1997.

[CKT95]

Coscoy Y., Kahn G., and Thery L. Extracting Text from Proofs. Technical Report RR-2459, Inria (Institut National de Recherche en Informatique et en Automatique), France, 1995.

[Coq86]

Coquand T. An Analysis of Girard's Paradox. In Symposium on Logic in Computer Science, Cambridge, 1986. MA. IEEE press.

[dBr80]

de Bruijn N. G. A survey of the project AUTOMATH. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pages 589--606. Academic Press, 1980.

[Geu93]

Geuvers H. Logics and Type Systems. Ph.D. dissertation, Catholic University Nijmegen, 1993.

[Gil60]

Gilmore P. C. A proof method for quantification theory: Its justification and realization. In IBM Journal of research and development, volume 4, pages 28--35, 1960.

[Gim94]

Giménez E. Codifying guarded definitions with recursive schemes. In Types'94: Types for Proofs and Programs, volume 996 of LNCS. Springer-Verlag, 1994. Extended version in LIP research report 95-07, ENS Lyon.

[Gim98]

Giménez E. A Tutorial on Recursive Types in Coq. Technical Report RT-0221, Inria (Institut National de Recherche en Informatique et en Automatique), France, 1998.

[GLT89]

Girard J. Y., Lafont Y., and Taylor P. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Har94]

Harrison J. The QED Manifesto. In Automated Deduction - CADE 12, volume 814 of Lecture Notes in Artificial Intelligence, pages 238--251. Springer-Verlag, 1994.

[Har96]

Harrison J. A Mizar Mode for HOL. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, pages 203--220, Turku, Finland, 1996. Springer-Verlag.

[HKP98]

Huet G., Kahn G., and Paulin-Mohring C. The Coq Proof Assistant. A Tutorial, 1998.

[Hor99]

Horacek H. Presenting Proofs in a Human Oriented Way. In 16th International Conference on Automated Deduction, 1999.

[ISO8879]

Standard Generalized Markup Language (SGML). ISO 8879:1986.

[Jut94]

Jutting van L. S. B. Checking Landau's ``Grundlagen'' in the AUTOMATH System. Ph d. thesis, Eindhoven University of Technology, 1994. Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732.

[Luo90]

Luo Z. An Extended Calculus of Constructions. PhD thesis, 1990.

[Mac95]

MacKenzie D. The automation of proof: A historical and sociological exploration. In IEEE: Annals of the History of Computing, 1995.

[Mas64]

Maslow S. J. An inverse method for establishing deducibility in classical predicate calculus. In Doklady Akademii Nauk, volume 159, pages 17--20, 1964.

[NL98]

Necula G. C. and Lee P. Efficient Representation and Validation of Proofs. In Proceedings of the 13th Annual symposium on Logic in Computer Science,, Indianapolis, 1998.

[NS56]

Newell A. and Simon H. A. The logic theory machine. In IRE Transactions on Information Theory, volume 2, pages 61--79, 1956.

[Pau89]

Paulin-Mohring C. Extraction de programmes dans le Calcul des Constructions. Thèse d'université, Paris 7, January 1989.

[Pra60]

Prawitz D. An improved proof procedure. In Theoria, volume 26, pages 102--139, 1960.

[Ric99]

Ricci A. Studio e progettazione di un modello RDF per biblioteche matematiche elettroniche, 1999.

[Rob65]

Robinson J. A. A machine-oriented logic based on the resolution principle. In Journal of the ACM, volume 2, pages 23--41, 1965.

[SH95]

Saibi A. and Huet G. Constructive Category Theory. In Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory, Goteborg (Sweden), January 1995.

[W3Ca]

Extensible Markup Language (XML) 1.0 W3C Reccomendation. http://www.w3.org/TR/1998/REC-xml-19980210.

[W3Cb]

Mathematical Markup Language (MathML) 1.01 W3C Reccomendation. http://www.w3.org/TR/REC-MathML.

[Wan60]

Wang H. Toward mechanical mathematics. In IBM Journal of research and development, volume 4, pages 2--22, 1960.

[Wer94]

Werner B. Une Théorie des Constructions Inductives. Ph.D. dissertation, Universite Paris 7, May 1994.

[Wer97]

Werner B. Constructive Category Theory. In Proocedings of the International Symposium on Theoretical Aspects of Computer Software, 1997.