From 2a81818cb4b942c35a1cfa88121e561309e59172 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 15 Nov 2005 18:14:57 +0000 Subject: [PATCH] - draft of the first part of disambiguation subsection - use bibtex --- helm/papers/matita/matita.bib | 1514 +++++++++++++++++++++++++++++++++ helm/papers/matita/matita.tex | 161 ++-- 2 files changed, 1605 insertions(+), 70 deletions(-) create mode 100644 helm/papers/matita/matita.bib diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib new file mode 100644 index 000000000..f98e9c431 --- /dev/null +++ b/helm/papers/matita/matita.bib @@ -0,0 +1,1514 @@ + +@inproceedings{gmetadom, + author = "Luca Padovani and Claudio Sacerdoti Coen and Stefano Zacchiroli", + title = "A Generative Approach to the Implementation of Language Bindings for the Document Object Model", + booktitle = "Generative Programming and Component Engineering", + editor = "Gabor Karsai and Eelco Visser", + series = "LNCS", + volume = "3286", + pages = "469--487", + publisher = "Springer-Verlag", + year = 2004, +} + +@techreport{mmode, + author = "Freek Wiedijk", + title = "MMode, a Mizar Mode for the proof assistant Coq", + institution = "University of Nijmegen", + number = "NIII-R0333", + year = "2003" +} + +@article{ lamport-proof, + author = "Leslie Lamport", + title = "How to write a proof", + journal = "American Mathematical Monthly", + volume = "102", + number = "7", + pages = "600--608", + year = "1995", +} + +@inproceedings{thery-authoring, + author = "Laurent Th\`ery", + title = "Formal Proof Authoring: an Experiment", + booktitle = "User Interface Design for Theorem Provers", + editor = "David Aspinall and Christoph L{\"u}th", + year = 2003 +} + +@inproceedings{padovani-editex, + author = "Luca Padovani", + title = "Interactive Editing of MathML Markup Using TeX Syntax", + booktitle = "International Conference on TeX, XML, and Digital Typography", + series = "LNCS", + volume = "3130,", + pages = "125--138", + year = 2004, + publisher = "Springer-Verlag", +} + +@inproceedings{uitp-knowledge-modelling, + author = "Stuart Aitken", + title = "Problem Solving in Interactive Proof: A Knowledge-Modelling Approach", + booktitle = "European Conference on Artificial Intelligence (ECAI)", + year = 1996 +} + +@inproceedings{proof-by-pointing, + author = "Yves Bertot", + title = "Proof by Pointing", + booktitle = "Symposium on Theoretical Aspects Computer Software (STACS)", + series = "Lecture Notes in Computer Science", + volume = "789", + year = 1993 +} + +@inproceedings{thery-cyp, + author = "Laurent Th\`ery", + title = "Colouring proofs: a lightweight approach to adding formal structure to proofs", + booktitle = "User Interface Design for Theorem Provers", + editor = "David Aspinall and Christoph L{\"u}th", + year = 2003 +} + +@article{uitp-empirical, + author = "Stuart Aitken and Phil Gray and Tom Melham and Muffy Thomas", + title = "Interactive Theorem Proving: An Empirical Study of User Activity", + journal = "Journal of Symbolic Computation", + year = 1995 +} + +@inproceedings{uitp-phases, + author = "Stuart Aitken and Phil Gray and Tom Melham and Muffy Thomas", + title = "Phases, Modes and Information Flow in Theory Development", + booktitle = "User Interface Design for Theorem Provers", + editor = "Nicholas Merriam", + year = 1996 +} + +@inproceedings{searchingmath, + author = "Andrea Asperti and Stefano Zacchiroli", + title = "Searching mathematics on the Web: state of the art and future developments", + booktitle = "New Developments in Electronic Publishing of Mathematics", + editor = "Bernd Wegner", + publisher = {FIZ Karlsruhe}, + YEAR = 2005 +} + +@article{fourcolor, + author = "K. Appel and W. Haken", + title = "Every planar map is four colorable.", + journal = {Illinois Journal of Mathematics}, + year = 1977, + volume = {21}, + pages = {429--567} +} + +@misc{freekcomparison, + author = "Freek Wiedijk", + title = "The Sixteen Provers of the World", + howpublished = "University of Nijmegen,\\\url{http://www.cs.ru.nl/~freek/comparison/comparison.ps.gz}" +} + +@misc{zmath, + title = "Zentralblatt MATH", + howpublished = "\url{http://www.emis.de/ZMATH/}" +} + +@inproceedings{lcf, + author = "Michael J. C. Gordon and Robin Milner and C.P. Wadsworth", + title = "{Edinburgh LCF}: a Mechanised Logic of Computation", + series = {Lecture Notes in Computer Science}, + volume = 78, + publisher = {{Sprin\-ger-Verlag}}, + year = 1979 +} + +@phdthesis{csc-phd, + author = "Claudio Sacerdoti Coen", + title = "Mathematical Knowledge Management and Interactive Theorem + Proving", + school = "University of Bologna", + year = "2004", + note = "Technical Report UBLCS 2004-5" +} + +@inproceedings{Isar, + author = "Markus Wenzel", + title = "Isar - A Generic Interpretative Approach to Readable Formal Proof Documents", + booktitle = "Theorem Proving in Higher Order Logics", + pages = "167-184", + year = "1999" +} + +@inproceedings{centaur, + author = "P. Borras and D. Clement and Th. Despeyrouz and J. Incerpi and G. Kahn and B. Lang and V. Pascual", + title = "{CENTAUR}: The System", + booktitle = "Proceedings of the {ACM} {SIGSOFT}/{SIGPLAN} Software Engineering Symposium on Practical Software Development Environments ({PSDE})", + journal = "SIGPLAN Notices", + volume = "24", + number = "2", + publisher = "ACM Press", + address = "New York, NY", + pages = "14--24", + year = "1989", + url = "citeseer.nj.nec.com/borras88centaur.html" +} + +@inproceedings{Leroy-manifest-types, + AUTHOR = "Xavier Leroy", + TITLE = "Manifest types, modules, and separate compilation", + BOOKTITLE = {21st symposium Principles of Programming Languages}, + YEAR = 1994, + PUBLISHER = {ACM Press}, + PAGES = {109--122}, + URL = {http://pauillac.inria.fr/~xleroy/publi/manifest-types-popl.ps.gz} +} + +@inproceedings{overkilling, + author = "Sacerdoti Coen, Claudio", + title = "Tactics in Modern Proof-Assistants: the Bad Habit of + Overkilling", + booktitle = "Supplementary Proceedings of the 14th International + Conference TPHOLS 2001", + pages = {352--367}, + year = 2001 +} + +@inproceedings{omegaants1, + author = "Christoph Benzm{\"u}ller and Volker Sorge", + title = {{OANTS} -- An open approach at combining Interactive and Automated + Theorem Proving}, + booktitle = {Symbolic Computation and Automated Reasoning}, + editor = {Manfred Kerber and Michael Kohlhase}, + year = 2000, + pages = {81--97}, + publisher = {A.K.Peters}, + url = {www.ags.uni-sb.de/~chris/papers/C8.pdf} +} + +@article{ocr, + author = "R. Fateman and T. Tokuyasu and B. Berman and N. Mitchell", + title = {Optical Character Recognition and Parsing of Typeset Mathematics}, + journal = {Journal of Visual Communication And Image Representation}, + year = 1996, + volume = {7}, + pages = {2--15}, + number = {1}, + month = mar, + url = {www.ags.uni-sb.de/~chris/papers/J4.pdf} +} + +@article{newauthomath, + author = "Freek Wiedijk", + title = "A new implementation of {A}utomath", + journal = {Journal of Automated Reasoning}, + year = 2002, + volume = {29}, + pages = {365--387} +} + +@article{gdome2, + author = "Paolo Casarini and Luca Padovani", + title = "The {G}nome {DOM} {E}ngine", + journal = "Markup Languages: Theory \& Practice", + year = 2002, + volume = {3}, + pages = {173--190}, + number = {2}, + publisher = "MIT Press", + month = apr +} + +@article{omegaants2, + author = "Christoph Benzm{\"u}ller and Mateja Jamnik and Manfred Kerber and + Volker Sorge", + title = {Agent based Mathematical Reasoning}, + journal = {Electronic Notes in Theoretical Computer Science, Elsevier}, + year = 1999, + volume = {23}, + pages = {21--33}, + number = {3}, + url = {www.ags.uni-sb.de/~chris/papers/J4.pdf} +} + +@inproceedings{Necula, + author = "George C. Necula and Peter Lee", + title = "Safe Kernel Extensions Without Run-Time Checking", + booktitle = "2nd Symposium on Operating Systems Design and Implementation ({OSDI} '96), October 28--31, 1996. Seattle, {WA}", + publisher = "USENIX", + address = "Berkeley, CA, USA", + editor = "{USENIX}", + pages = "229--243", + year = "1996", + url = "citeseer.nj.nec.com/necula96safe.html" +} + +@inproceedings{courant, + AUTHOR = "Judica{\"e}l Courant", + TITLE = {Explicit Universes for the {C}alculus of {C}onstructions}, + BOOKTITLE = {Theorem Proving in Higher Order Logics: + 15th International Conference, TPHOLs 2002}, + EDITOR = {Victor A. {Carre\~{n}o} and C\'{e}sar A. {Mu\~{n}oz} and Sofi\`{e}ne Tahar}, + SERIES = {Lecture Notes in Computer Science}, + VOLUME = 2410, + PAGES = {115--130}, + YEAR = 2002, + PUBLISHER = {{Sprin\-ger-Verlag}}, + MONTH = AUG, + ADDRESS = {Hampton, VA, USA} +} + +@inproceedings{NL98, + author = "George C. Necula and Peter Lee", + title="{Efficient Representation and Validation of Proofs}", + booktitle="Proceedings of the 13th Annual symposium on Logic in Computer Science,", + address="Indianapolis", + year="1998" +} + +@book{GirardJY:prot, + author = "Jean-Yves Girard and Yves Lafont and Paul Taylor", + title = "{Proofs and Types}", + publisher = {Cambridge University Press}, + series = {Cambridge Tracts in Theoretical Computer Science}, + year = 1989 +} + +@inproceedings{proofgeneral, + author = "David Aspinall", + title = "{P}roof {G}eneral: A Generic Tool for Proof Development", + booktitle = "Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000", + series = "LNCS", + volume = "1785", + month = jan, + year = 2000, + publisher = "Springer-Verlag", +} + +@inproceedings{Gim94, + author = "Eduardo Gim\'enez", + title = "{Codifying guarded definitions with recursive schemes}", + booktitle = "Types'94: Types for Proofs and Programs", + series = "LNCS", + volume = 996, + year = 1994, + publisher = "Springer-Verlag", + note = "Extended version in LIP research report 95-07, ENS Lyon", + pages = "39--59", +} + +@incollection{BarendregtH:lawcwt, + author = "H. Barendregt", + title = "{Lambda Calculi with Types}", + booktitle = "{Handbook of Logic in Computer Science}", + editor = "{Abramsky, Samson and others}", + publisher = "{Oxford University Press}", + volume = 2, + year = 1992 +} + +@inproceedings{coquand:1986, + author="Thierry Coquand", + title="{An Analysis of Girard's Paradox}", + booktitle="Symposium on Logic in Computer Science", + address="Cambridge", + publisher="MA. IEEE press", + year="1986" +} + +@phdthesis{mohring, + AUTHOR = "Christine Paulin-Mohring", + TITLE = {D\'efinitions Inductives en Th\'eorie des Types d'Ordre Sup\'rieur}, + SCHOOL = {Universit\'e Claude Bernard Lyon I}, + YEAR = 1996, + MONTH = DEC, + TYPE = {Habilitation \`a diriger les recherches}, + URL = {http://www.lri.fr/~paulin/habilitation.ps.gz} +} + +@phdthesis{garrigue, + author = "Jacques Garrigue", + title = "{Label-Selective Lambda-Calculi and Transformation Calculi}", + school = "University of Tokyo, Department of Information Science", + month = mar, + year = 1995 +} + +@phdthesis{LuoZ:extcc, + author = "Zhaohui Luo", + title = "{An Extended Calculus of Constructions}", + school = "University of Edinburgh", + year = 1990 +} + +@phdthesis{chicly, + author = "Laurent Chicli", + title = "Sur la formalisation des math\'ematiques dans le + {C}alcul des {C}onstructions {I}nductives", + school = "Universit\'e de Nice~-~Sophia Antipolis", + year = 2003 +} + +@phdthesis{geuvers:1993, + author="Herman Geuvers", + title="{Logics and Type Systems}", + school="Catholic University Nijmegen", + year="1993", + type="{Ph.D.} dissertation" +} + +@unpublished{PrimesInP, + author = "M. Agrawal and N. Kayal and N. Saxena", + title = "{PRIMES} in {P}", + note = "\url{http://www.cse.iitk.ac.in/users/manindra/primality.ps}", + month = aug, + year = 2002 +} + +@unpublished{danosKAM, + author = "Vincent Danos and Laurent Regnier", + title = "How abstract machines implement head linear reduction", + year = 2003 +} + +@inproceedings{Oostdijk, + author = "Olga Caprotti and Herman Geuvers and Martin Oostdijk", + title = "Certified and Portable Mathematical Documents from Formal Contexts", + editor = "Bruno Buchberger and Olga Caprotti", + booktitle = "On-Line Proceedings of the First International Conference on + Mathematical Knowledge Management, MKM 2001", + publisher = "The Electronic Library of Mathematics (EMIS)", + url = "\url{http://www.emis.de/ELibM.html}", + year = "2001" +} + +@inproceedings{formal-proof-sketches, + author = "Freek Wiedijk", + title = "Formal Proof Sketches", + editor = "Wan Fokkink and Jaco van de Pol", + booktitle = "7th Dutch Proof Tools Day, Program + Proceedings", + note = "CWI, Amsterdam", + year = "2003", +} + +@inproceedings{Barendregt, + author = "Henk Barendregt", + title = "Towards an Interactive Mathematical Proof Language", + editor = "Fairouz Kamareddine", + booktitle = "Thirty Five Years of Automath", + pages = "25--36", + publisher = "Kluwer", + year = "2003", +} + +@inproceedings{werner:prof-irrelevance, + author = "Alexandre Miquel and Benjamin Werner", + title = "The Not So Simple Proof-Irrelevant Model of {CC}", + editor = "Herman Geuvers and Freek Wiedijk", + booktitle = "Types for Proofs and Programs: International Workshop, TYPES 2002", + pages = "240--258", + volume = "LNCS, 2646", + publisher = "Springer-Verlag", + year = "2003", +} + +@inproceedings{csc-environment, + author = "Claudio Sacerdoti Coen", + title = "Mathematical Libraries as Proof Assistant Environments", + editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec", + booktitle = "Proceedings of Mathematical Knowledge Management 2004", + volume = "LNCS, 3119", + pages = "332--346", + publisher = "Springer-Verlag", + year = "2004" +} + +@inproceedings{disambiguation, + author = "Claudio Sacerdoti Coen and Stefano Zacchiroli", + title = "Efficient Ambiguous Parsing of Mathematical Formulae", + editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec", + booktitle = "Proceedings of Mathematical Knowledge Management 2004", + volume = "LNCS, 3119", + pages = "347--362", + publisher = "Springer-Verlag", + year = "2004" +} + +@inproceedings{pechino, + author = "Andrea Asperti and Bernd Wegner", + title = "An Approach to Machine-Understandable Representation of the Mathematical Information in Digital Documents", + editor = "Fengshai Bai and Bernd Wegner", + booktitle = "Electronic Information and Communication in Mathematics", + volume = "LNCS, 2730", + pages = "14--23", + publisher = "Springer-Verlag", + year = "2003" +} + +@inproceedings{whelp, + author = "Andrea Asperti and Ferruccio Guidi and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli", + title = "A content based mathematical search engine: Whelp", + booktitle = "Post-proceedings of the Types 2004 International Conference", + volume = "LNCS, (to appear)", + pages = "xxx--xxx", + publisher = "Springer-Verlag", + year = "2004" +} + +@inproceedings{exportation-module, + author = "Sacerdoti Coen, Claudio", + title = "From Proof-Assistans to Distributed Libraries of Mathematics: Tips + and Pitfalls", + editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport", + booktitle = "Proceedings of the Second International Conference on + Mathematical Knowledge Management, MKM 2003", + pages = "30--44", + volume = "LNCS, 2594", + publisher = "Springer-Verlag", + year = "2003", +} + +@inproceedings{ida, + author = "Andrea Asperti and Herman Geuvers and Iris Loeb and Lionel Elie Mamane and Claudio Sacerdoti Coen", + title = "An Interactive Algebra Course with Formalised Proofs and Definitions", + editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport", + booktitle = "Post-Proceedings of the Fourth International Conference on Mathematical Knowledge Management, MKM 2005", + pages = "XXX--XXX", + volume = "LNCS, (to appear)", + publisher = "Springer-Verlag", + year = "2005", +} + +@inproceedings{davenport, + author = "James H. Davenport", + title = "{MKM} from Book to Computer: A Case Study", + editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport", + booktitle = "Proceedings of the Second International Conference on + Mathematical Knowledge Management, MKM 2003", + pages = "17--29", + volume = "LNCS, 2594", + publisher = "Springer-Verlag", + year = "2003", +} + +@inproceedings{fguidisacerdot, + author = "Ferruccio Guidi and Sacerdoti Coen, Claudio", + title = "Querying Distributed Digital Libraries of Mathematics", + editor = "Therese Hardin and Renaud Rioboo", + booktitle = "Calculemus 2003", + pages = "17--30", + publisher = "Aracne Editrice S.R.L.", + year = "2003", + note = "ISBN 88-7999-545-6" +} + +@inproceedings{hbugs, + author = "Sacerdoti Coen, Claudio and Stefano Zacchiroli", + title = "Brokers and {W}eb-Services for Automatic Deduction: a Case Study", + editor = "Therese Hardin and Renaud Rioboo", + booktitle = "Calculemus 2003", + pages = "43--57", + publisher = "Aracne Editrice S.R.L.", + year = "2003", + note = "ISBN 88-7999-545-6" +} + +@inproceedings{calculemus-presentation, + author = "Christoph Benzm{\"u}ller", + title = "The {CALCULEMUS} Research Training Network -- A short Overview", + editor = "Therese Hardin and Renaud Rioboo", + booktitle = "Calculemus 2003", + pages = "1--16", + publisher = "Aracne Editrice S.R.L.", + year = "2003", + note = "ISBN 88-7999-545-6" +} + +@inproceedings{linda, + author = "Sacerdoti Coen, Claudio", + title = "A Constructive Proof of the Soundness of the + Encoding of Random Access Machines in a Linda Calculus with Ordered + Semantics", + booktitle = "Theoretical Computer Science: 8th Italian Conference, ICTCS 2003", + pages = "37--57", + volume = "LNCS, 2841", + publisher = "Springer-Verlag", + year = "2003", +} + + +@article{asperti-categorical-understanding, + author = "Andrea Asperti", + title = "A categorical understanding of environment machines", + journal = "Journal of Functional Programming", + volume = "2", + number = "1", + pages = "23--59", + month = jan, + year = "1992" +} + +@article{namelessdummies, + author = "{N. G. de Bruijn}", + title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem", + journal = "Indagationes Mathematicae", + volume = "34", + pages = "381--392", + year = "1972" +} + +@article{ctcoq1, + author = "Yves Bertot", + title = "The CtCoq System: Design and Architecture", + journal = "Formal Aspects of Computing", + volume = "11", + pages = "225--243", + year = "1999" +} + +@article{ctcoq3, + author = "Yves Bertot and Laurent Th\'ery", + title = "A Generic Approach to Building User Interfaces for Theorem Provers", + journal = "Journal of Symbolic Computation", + volume = "25", + pages = "161--194", + year = "1998" +} + +@article{mbase, + author = "Michael Kohlhase and Andreas Franke", + title = "{MBase}: Representing Knowledge and Context for the Integration of Mathematical Software Systems", + journal = "Journal of Symbolic Computation", + volume = "32", + number = "4", + pages = "365--402", + year = "2001", + url = "\url{http://citeseer.nj.nec.com/kohlhase00mbase.html}" +} + +@inproceedings{mizarql, + author = "Grzegorz Bancerek and Piotr Rudnicki", + title = "Information Retrieval in {MML}", + editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport", + booktitle = "Proceedings of the Second International Conference on + Mathematical Knowledge Management, MKM 2003", + pages = "119--132", + volume = "LNCS, 2594", + publisher = "Springer-Verlag", + year = "2003", +} + +@article{codedcontexttrees, + author = "Harald Ganzinger and Robert Nieuwehuis and Pilar Nivela", + title = "Fast Term Indexing with Coded Context Trees. Journal of Automated Reasoning", + journal = "Journal of Automated Reasoning", + year = "To appear" +} + +@article{ranta, + author = "Aarne Ranta", + title = "Grammatical Framework: A Type-Theoretical Grammar Formalism", + journal = "Journal of Functional Programming", + year = "To appear", + note = "Manuscript made available in September 2002" +} + +@book{DiCosmo, + AUTHOR = "Di Cosmo, Roberto", + TITLE = {Isomorphisms of types: from $\lambda$-calculus to information retrieval and language design}, + SERIES = {Progress in Theoretical Computer Science}, + PUBLISHER = {Birkhauser}, + YEAR = {1995}, + NOTE = {ISBN-0-8176-3763-X} +} + +@book{automath, + EDITOR = "R.P. Nederpelt and J.H. Geuvers and R.C. de Vrijer", + TITLE = {Selected Papers on Automath}, + SERIES = {Studies in Logic and the Foundations of Mathematics}, + PUBLISHER = {Elsevier Science}, + VOLUME = "133", + YEAR = {1994}, + NOTE = {ISBN-0444898220} +} + +@misc{krivine, + author = "Jean-Louis Krivine", + title = "Un interpr\`ete du $\lambda$-calcul", + howpublished = "Brouillon. Available on-line at \url{http://www.logique.jussieu.fr/~krivine}", + year = 1985 +} + +@misc{na-mkm1, + title = "Progress Report: Building Interactive Digital Libraries of Formal + Algorithmic Knowledge", + howpublished = "Cornell University, \url{http://www.cs.uwyo.edu/~nuprl/documents/cornell_slides.pdf}", + month = may, + year = 2002, + key = "Progress" +} + +@misc{metadata4education, + title = "{L}earning {O}bject {M}etadata Standard", + howpublished = "Learning Technology Standards Committee of IEEE, \verb+http://www.learninglab.de/elan/kb3/lexikon/metadaten-standards/docs/+ \verb+LOM_1484_12_1_v1_Final_Draft.pdf+", + year = 2002, + key = "Learning" +} + +@misc{openmath-cd-with-plus, + title = "Arith1 {OpenMath} {C}ontent {D}ictionary", + howpublished = "The OpenMath Society, \url{http://www.openmath.org/cocoon/openmath/cd/arith1.ocd}", + year = 2002, + key = "Arith1 OpenMath Content Dictionary" +} + + +@misc{ddc, + title = "Dewey Decimal Classification", + howpublished = "\url{http://www.oclc.org/dewey}", + url = "\url{http://www.oclc.org/dewey}", + key = "Dewey" +} + +@misc{lc, + title = "Library of Congress Classification Scheme", + howpublished = "\url{http://www.loc.gov}", + url = "\url{http://www.loc.gov}", + key = "Library" +} + +@misc{msc, + title = "Mathematical {S}ubject {C}lassification, {A}merican {M}athematical {S}ociety", + howpublished = "\url{http://www.ams.org/msc}", + url = "\url{http://www.ams.org/msc}", + key = "Mathematical" +} + +@InCollection{borges, + author = "Jorge Luis Borges", + title = "The Library of {B}abel", + publisher = "Grove Press", + booktitle = "Ficciones", + year = 1942 +} + +@inproceedings{magaud, + author = "Nicolas Magaud", + title = "{C}hanging {D}ata {R}epresentation within the {C}oq {S}ystem", + booktitle = {TPHOLs'2003}, + publisher = {Springer-Verlag}, + volume = {LNCS, 2758}, + year = {2003}, +} + +@inproceedings{geuvers-jojgov, + author = "Herman Geuvers and Gueorgui I. Jojgov", + title = "Open Proofs and Open Terms: A Basis for Interactive Logic", + editor = "J. Bradfield", + booktitle = "Computer Science Logic: 16th International Workshop, CLS 2002", + pages = "537-552", + volume = "LNCS, 2471", + publisher = "Springer-Verlag", + month = jan, + year = "2002" +} + +@inproceedings{mkm-structure, + author = "Koji Nakagawa and Akihiro Nomura and Masakazu Suzuki", + title = "Extraction of Logical Structure from articles in Mathematics", + editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec", + booktitle = "Proceedings of Mathematical Knowledge Management 2004", + volume = "LNCS, 3119", + pages = "276--289", + publisher = "Springer-Verlag", + year = "2004" +} + +@inproceedings{mkm-metadata2, + author = "Andrea Asperti and Matteo Selmi", + title = "Efficient Retrieval of Mathematical Statements", + editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec", + booktitle = "Proceedings of Mathematical Knowledge Management 2004", + volume = "LNCS, 3119", + pages = "17--31", + publisher = "Springer-Verlag", + year = "2004" +} + +@inproceedings{adams, + author = "A. A. Adams", + title = "Digitisation, Representation and Formalisation: Digital + Libraries of Mathematics.", + editor = "A. Asperti, B. Buchberger, J.H. Davenport", + booktitle = "Proceedings of Mathematical Knowledge Management 2003", + volume = "LNCS, 2594", + pages = "1--16", + publisher = "Springer-Verlag", + year = "2003" +} + +@inproceedings{maya, + author = "Serge Autexier and Dieter Hutter and Heiko Mantel and Axel Schairer", + title = "Towards an Evolutionary Formal Software-Development Using {CASL}", + booktitle = "WADT99 Selected Papers Volume", + volume = "LNCS, 1827", + publisher = "Springer-Verlag", + year = "2000" +} + +@inproceedings{how-to-extract, + author = "Lu\'is Cruz Filipe and Bas Spitters", + title = "Program Extraction from large proof developments", + booktitle = "Proceedings of TPHOLS 2003", + editor = "D. Basin and B. Wolff", + volume = "LNCS, 2758", + publisher = "Springer-Verlag", + year = "2003" +} + +@inproceedings{click-and-prove, + author = "Jean-Raymond Abrial and Dominique Cansell", + title = "Click'n {P}rove: Interactive Proofs Within Set Theory", + booktitle = "Proceedings of TPHOLS 2003", + editor = "D. Basin and B. Wolff", + volume = "LNCS, 2758", + publisher = "Springer-Verlag", + year = "2003" +} + +@inproceedings{delahaye, + author = "David Delahaye and Roberto di Cosmo", + title = "Information Retrieval in a {C}oq Proof Library using + Type Isomorphisms", + booktitle = "Proceedings of TYPES 99", + volume = "LNCS", + publisher = "Springer-Verlag", + year = "1999" +} + +@TechReport{jojgov, + author = "G. I. Jojgov", + title = "Systems for open terms: An Overview", + institution = "Technische Universiteit Eindhoven", + number = "CSR 01-03", + year = "2001" +} + +@TechReport{garrigue:implicit-arguments, + author = "Jun P. Furuse and Jacques Garrigue", + title = " A label-selective lambda-calculus with optional arguments and its compilation method", + institution = "Research Institute for Mathematical Sciences, Kyoto University", + number = "RIMS Preprint 1041", + month = oct, + year = "1995" +} + +@phdthesis{miquel, + author = "Alexandre Miquel", + title = "Le {C}alcul des {C}onstructions {I}mplicite: syntaxe et s\'emantique", + school = "Universit\'e Paris 7", + year = "2001" +} + +@phdthesis{chrzaszcz, + author = "Jacek Chrz{\c{a}}szcs", + title = "Modules in Type Theory with Generative Definitions", + school = "Uniwersytet Warszawski and Universit\'e de Paris Sud", + year = "2003" +} + +@phdthesis{Pons, + author = "Olivier Pons", + title = "Conception et r\'ealisation d'outils d'aide au d\'eveloppement de grosse th\'eories dans les syst\`emes de preuves interactifs", + school = "Conservatoire National des Arts et M\'etiers", + year = "1999" +} + +@phdthesis{blanqui, + author = "Fr\'ed\'eric Blanqui", + title = "Type Theory and Rewriting", + school = "Universit\'e Paris XI", + year = "2001" +} + +@phdthesis{magnusson, + author = "Lena Magnusson", + title = "The Implementation of {ALF} -- a Proof Editor based + on Martin-L{\"o}f Monomorphic Type Theory with Explicit + Substitutions", + school = "Chalmers University of Technology / G{\"o}teborg University", + year = "1995" +} + +@phdthesis{McBride, + author = "Conor McBride", + title = "Dependently Typed Functional Programs and their Proofs", + school = "University of Edinburgh", + year = "1999" +} + +@phdthesis{schena, + author = "Irene Schena", + title = "Towards a Semantic Web for Formal Mathematics", + school = "University of Bologna", + year = "2002" +} + +@phdthesis{fguidi, + author = "Ferruccio Guidi", + title = "Searching and Retrieving in Content-Based Repositories + of Formal Mathematical Knowledge", + school = "University of Bologna", + month = mar, + year = "2003", + note = "Technical Report UBLCS 2003-06" +} + +@phdthesis{padovani, + author = "Luca Padovani", + title = "MathML Formatting", + school = "University of Bologna", + month = feb, + year = "2003", + note = "Technical Report UBLCS 2003-03" +} + +@mastersthesis{csc-master, + author = "Sacerdoti Coen, Claudio", + title = "Progettazione e realizzazione con tecnologia {XML} di basi distribuite di conoscenza matematica formalizzata", + school = "University of Bologna", + year = 2000 +} + +@mastersthesis{zack-master, + author = "Stefano Zacchiroli", + title = "Web {s}ervices per il supporto alla dimostrazione interattiva", + school = "University of Bologna", + year = 2003 +} + +@mastersthesis{dilena, + author = "Pietro Dilena", + title = "Generazione automatica di stylesheet per notazione matematica", + school = "University of Bologna", + year = 2003 +} + +@phdthesis{munoz, + author = "C\'esar Munoz", + title = "A Calculus of Substitutions for Incomplete-Proof + Representation in Type Theory", + school = "INRIA", + month = nov, + year = "1997" +} + +@phdthesis{strecker, + author = "Martin Strecker", + title = "Construction and Deduction in Type Theories", + school = "Universit{\"a}t Ulm", + year = 1998 +} + + +@misc{mowgli-proposal, + title = "The {MoWGLI Proposal}, {HTML} Version", + howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/project.html}", + key = "MoWGLI Proposal" +} + +@misc{mowgli-deliverables, + title = "{MoWGLI} Project Deliverables", + howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html}", + key = "MoWGLI Deliverables" +} + +@misc{ALF, + title = "The {ALF} family of proof-assistants", + howpublished = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}", + url = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}", + key = "ALF" +} + +@misc{Coq, + title = "The {C}oq proof-assistant", + howpublished = "\\\url{http://coq.inria.fr}", + key = "Coq" +} + +@misc{phox, + title = "The {PhoX} proof-assistant", + howpublished = "\\\url{http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html}", + key = "PhoX" +} + +@misc{lego, + title = "The {L}ego proof-assistant", + howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}", + url = "\url{http://www.dcs.ed.ac.uk/home/lego/}", + key = "Lego" +} + +@misc{ALFA, + title = "The {A}lfa proof editor", + howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}", + url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}", + key = "Alfa" +} + +@misc{pvs, + title = "The {PVS} Specification and Verification System", + howpublished = "\\\url{http://pvs.csl.sri.com/}", + key = "PVS" +} + +@misc{isabelle, + title = "The {Isabelle} proof-assistant", + howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}", + key = "Isabelle" +} + +@misc{nuprl, + title = "The {NuPRL} proof-assistant", + howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}", + key = "NuPRL" +} + +@misc{hollight, + title = "The {HOL Light} proof-assistant", + howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}", + key = "HOL-Light" +} + +@misc{monet, + title = "The {MONET} project", + howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}", + key = "Monet" +} + +@misc{calculemus, + title = "The {CALCULEMUS} project", + howpublished = "\url{http://www.calculemus.net/}", + url = "\url{http://www.calculemus.net/}", + key = "Calculemus" +} + +@misc{mizar, + title = "The {M}izar proof-assistant", + howpublished = "\\\url{http://mizar.uwb.edu.pl/}", + key = "Mizar" +} + +@misc{openmath, + howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium", + author = "O. Caprotti and D. P. Carlisle and A. M. Cohen", + title = "{\emph{The {O}pen{M}ath {S}tandard}}" +} + +@misc{mathml, + title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0", + editor="{Patrick Ion} and others", + howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}", + url = "\url{http://www.w3.org/TR/MathML2}", + key = "Mathematical" +} + +@misc{xml, + title = "{E}xtensible {M}arkup {L}anguage ({XML}). {V}ersion 1.0.", +editor="{Tim Bray} and others", + howpublished = "W3C Recommendation 10 February 1998, + \url{http://www.w3.org/TR/REC-xml}", + url = "\url{http://www.w3.org/TR/REC-xml}", + key = "Extensible" +} + +@misc{dom, + title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0", + howpublished = "W3C Candidate Recommendation 10 May 2000, + \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}", + url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}", + key = "Document" +} + +@misc{URIs, + title = "Universal Resource Identifiers in {WWW}", + howpublished = "RFC 1630, CERN", + month = jun, + year = "1994", + key = "URI" +} + +@misc{xpath, + title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0", + howpublished = "W3C Recommendation, 16 November 1999, + \url{http://www.w3.org/TR/xpath}", + url = "\url{http://www.w3.org/TR/xpath}", + key = "XML" +} + +@misc{xslt, + title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0", + howpublished = "W3C Recommendation, 16 November 1999, + \url{http://www.w3.org/TR/xslt}", + url = "\url{http://www.w3.org/TR/xslt}", + key = "XSLT" +} + +@misc{rdf, + title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax + Specification", + howpublished = "W3C Recommendation 22 February 1999, + \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}", + url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}", + key = "Resource" +} + +@misc{omdoc, + title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)", + howpublished = "\\\url{http://www.mathweb.org/omdoc/omdoc.ps}", + key = "OMDoc" +} + +@misc{FORMAVIE, + title = "The {F}ormavie project", + howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}", + url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}", + key = "Formavie" +} + +@misc{EHELM, + title = "The {HELM} project", + howpublished = "\url{http://helm.cs.unibo.it}", + url = "\url{http://helm.cs.unibo.it}", + key = "HELM" +} + +@misc{helm-library, + title = "The {HELM} On-Line Library", + howpublished = "\url{http://helm.cs.unibo.it/library.html}", + url = "\url{http://helm.cs.unibo.it/library.html}", + key = "HELM Library" +} + +@misc{MATHWEB, + title = "The {M}ath{W}eb project", + howpublished = "\url{http://www.mathweb.org}", + url = "\url{http://www.mathweb.org}", + key = "MathWeb" +} + +@misc{PCOQ, + title = "The {PC}oq project", + howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}", + url = "\url{http://www-sop.inria.fr/lemme/pcoq}", + key = "PCoq" +} + +@TechReport{HELM, + author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen + and Irene Schena", + title = "Towards a library of formal mathematics", + year = "2000", + note = "Panel session of the 13th {I}nternation {C}onference on + {T}heorem {P}roving in {H}igher {O}rder {L}ogics + ({TPHOLS}'2000), Portland, Oregon, USA", +} + +@TechReport{ctcoq2, + author = "Laurent Th\'ery and Yves Bertot and Gilles Kahn", + title = "Real Theorem Provers Deserve Real User-Interfaces", + month = may, + year = "1992", + institution = "INRIA", + number = "{Inria Research Report 1684}" +} + +@inproceedings{Ring, + author = "Samuel Boutin", + title = "Using Reflection to Build Efficient and Certified Decision + Procedures", + editor = "Martin Abadi and Takahashi Ito editors", + booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS", + pages = "515-529", + volume = "1281", + publisher = "Springer-Verlag", + year = "1997", +} + +@inproceedings{werner-zfc, + author = "Benjamin Werner", + title = "Sets in Types, Types in Sets", + editor = "Martin Abadi and Takahashi Ito editors", + booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS", + pages = "530-546", + volume = "1281", + publisher = "Springer-Verlag", + year = "1997", +} + +@article{aczel, + author = "Peter Aczel", + title = "On Relating Type Theories and Set Theories", + journal = "Lecture Notes in Computer Science", + volume = "1657", + year = "1999", +} + +@inproceedings{remathematization, + author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena", + title = "{XML}, Stylesheets and the re-mathematization of Formal Content", + booktitle = "EXTREME", + year = "2001", +} + + +@phdthesis{YANNTHESIS, + author = "Yann Coscoy", + title = "Explication textuelle de preuves pour le {C}alcul des + {C}onstructions {I}nductives", + school = "Universit\'e de Nice-Sophia Antipolis", + year = "2000", +} + +@phdthesis{Lippi, + author = "Sylvain Lippi", + title = "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)", + school = "Universit\'e Aix-Marseille 2", + year = "2002" +} + +@phdthesis{Werner, + author = "Benjamin Werner", + title = "Une Th\'eorie des {C}onstructions {I}nductives", + school = "Universit\'e Paris VII", + month = may, + year = "1994", +} + +@InCollection{Felleisen87, + author = "M. Felleisen and D. Friedman", + editor = "M. Wirsing", + title = "Control operators, the {SECD}-machine, and the lambda calculus", + booktitle = "Formal Description of Programming Concepts III", + pages = "193--217", + publisher = "Elsevier Science Publishers B.V.", + address = "(North-Holland) Amsterdam", + year = "1987", +} + +@TechReport{yarrow, + author = "Jan Zwanenburg", + institution = "Eindhoven University of Technology", + number = "Computing Science Report CS-98-11", + title = "The Proof-assistant Yarrow", + year = "1998" +} + +@TechReport{Ager2003a, + author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard", + institution = "BRICS", + month = mar, + number = "BRICS RS-03-13", + title = "A Functional Correspondence between Evaluators and Abstract Machines", + year = "2003" +} + +@TechReport{Ager2003b, + author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard", + institution = "BRICS", + month = mar, + number = "BRICS RS-03-14", + title = "From Interpreter to Compiler and Virtual Machine: A Functional Derivation", + year = "2003" +} + +@article{harperpollack, + author = "Robert Harper and Robert Pollack", + title = "Type checking with universes", + journal = "Theoretical Computer Science", + volume = "89", + pages = "107--136", + year = "1991" +} + +@article{activemath, + author = "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich", + title = "Knowledge Representation and Management in {ActiveMath}", + journal = "Annals of Mathematics and Artificial Intelligence", + volume = "38(1-3)", + pages = "47--64", + month = may, + year = "2003" +} + +@article{mkm-helm, + author = "Andrea Asperti and Ferruccio Guidi and Luca Padovani and + Claudio Sacerdoti Coen and Irene Schena", + title = "Mathematical Knowledge Management in {HELM}", + journal = "Annals of Mathematics and Artificial Intelligence", + volume = "38(1-3)", + pages = "27--46", + month = may, + year = "2003" +} + +@unpublished{formal-topology, + author = "Giovanni Sambin", + title = "Some points in formal topology", + note = "To appear in Theoretical Computer Science", + year = "2002" +} + +@TechReport{JohnHarrison:complexity-of-floating-point-proofs, + author = "John Harrison", + title = "Real Numbers in Real Applications", + note = "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002", + institution = "NASA", + number = "NASA/CP-2002-211736", + year = "2002" +} + +@inproceedings{kohlhase-anghelache, + author = "Michael Kohlhase and Romeo Anghelache", + title = "Towards Collaborative Content Management And Version Control For + Structured Mathematical Knowledge", + editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport", + booktitle = "Proceedings of the Second International Conference on + Mathematical Knowledge Management, MKM 2003", + pages = "147--161", + volume = "LNCS, 2594", + publisher = "Springer-Verlag", + year = "2003", +} + +%%% Unused entries from my Master dissertation bibliography + +@misc{sgml, + title="{Standard Generalized Markup Language (SGML)}", + note="ISO 8879:1986", + key="ISO" + } + +@unpublished{helm1, + author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena", + title = "{Content Centric Logical Environments}", + note = "Short Presentation at LICS 2000", + ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz", +} + +@unpublished{helm4, + author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena", + title = "{Formal Mathematics in MathML}", + note = "To be presented at MathML International Conference 2000", +} + +@unpublished{helm2, + author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena", + title = "{Towards a Library of Formal Mathematics}", + note = "Accepted at TPHOLS 2000", + ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz", +} + +@techreport{mowgli:D4a, + author = "Hanane Naciri and Luca Padovani", + title = "{MathML} Rendering/Browsing Engine", + type = {MoWGLI Report}, + number = {D4a}, + year = 2003, + howpublished = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}" +} + +@techreport{hazewinkel, + author = "Michiel Hazewinkel", + title = "Dynamic stochastic models for indexes and thesauri, + identification clouds, and information retrieval and + storage", + type = "{MKM Net Report}", + howpublished = "\url{http://monet.nag.co.uk/mkm//index.html}" +} + +@techreport{BarrasB:coqpar, + author = "{Barras B.} and {Boutin S.} and {Cornes C.} + and {Courant J.} and {Filliatre J. C.} + and {Gim\'enez E.} and {Herbelin H.} and {Huet G.} + and {Munoz C.} and {Murthy C.} and {Parent C.} + and {Paulin-Mohring C.} and {Saibi A.} + and {Werner B.}", + title = "{The Coq Proof Assistant Reference Manual : Version + 6.1}", + institution = {Inria (Institut National de Recherche en Informatique + et en Automatique), France}, + type = {Technical Report}, + number = {RT-0203}, + year = 1997, + author_acronym = {WernerB}, + bibdate = {May 1, 1997}, + source = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/}, + source-date = {Mon 11 Sep 100}, + title_acronym = {coqpar} +} + +@unpublished{bw:1997, + author = "Bruno Barras and Benjamin Werner", + title = "{Coq in Coq}", + year = "1997", + note = "Submitted", + ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz", +} + +@unpublished{berners-lee:1989, + author = "Tim Berners-Lee", + title = "{Information Management: A Proposal}", + year = "1989", + ps = "http://www.w3.org/History/1989/proposal.html", +} + +@techreport{natural, + author = "Yann Coscoy and Gilles Kahn and Laurent Thery", + title = "{Extracting Text from Proofs}", + institution = {Inria (Institut National de Recherche en Informatique + et en Automatique), France}, + type = {Technical Report}, + number = {RR-2459}, + year = 1995 +} + +@inproceedings{Bru80, + author = "de Bruijn, N. G.", + title = "{A survey of the project AUTOMATH}", + pages = "589--606", + editor = "J. P. Seldin and J. R. Hindley", + booktitle = "To H. B. Curry: Essays in Combinatory Logic, + Lambda Calculus and Formalism", + year = 1980, + publisher = "Academic Press" +} + +@techreport{tutrect, + author = "E Gim\'enez", + title = "{A Tutorial on Recursive Types in Coq}", + institution = {Inria (Institut National de Recherche en Informatique + et en Automatique), France}, + type = {Technical Report}, + number = {RT-0221}, + year = 1998 +} + +@inproceedings{QED, + author = "John Harrison", + title = "{The QED Manifesto}", + pages = "238--251", + booktitle = "Automated Deduction - CADE 12", + series = "Lecture Notes in Artificial Intelligence", + volume = 814, + year = 1994, + publisher = "Springer-Verlag" +} + +@inproceedings{harrison-mizar, + author = "John Harrison", + title = "{A Mizar Mode for HOL}", + pages = "203--220", + editor = "Joakim von Wright and Jim Grundy and John Harrison", + booktitle = "Theorem Proving in Higher Order Logics: + 9th International Conference, TPHOLs'96", + series = "Lecture Notes in Computer Science", + volume = 1125, + address = "Turku, Finland", + date = "26--30 August 1996", + year = 1996, + publisher = "Springer-Verlag" +} + +@inproceedings{proverb, + author="H. Horacek", + title="{Presenting Proofs in a Human Oriented Way}", + booktitle="16th International Conference on Automated Deduction", + year="1999" + } + +@misc{HuetG:coqpat, + author = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring", + title = "{The Coq Proof Assistant. A Tutorial}", + year = 1998 +} + +@PHDTHESIS{BJ94, + author="{Jutting van L. S. B.}", + school = {{Eindhoven University of Technology}}, + title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}", + type = {Ph D. thesis}, + note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}", + year = {1994} +} + +@misc{abriefhistoryoftheinternet, + author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.} + and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.} + and {Postel J.} and {Roberts L. G.} and {Wolff S.}", + title="{A Brief Hystory of the Internet}", + note="http://www.isoc.org/internet-history/brief.html" + } + +@inproceedings{MacKenzie:1995, + author="{MacKenzie D.}", + title="{The automation of proof: A historical and sociological exploration}", + booktitle="IEEE: Annals of the History of Computing", + year="1995" +} + +@PHDTHESIS{Moh89b, + author = "Christine Paulin-Mohring", + month = {January}, + school = {{Paris 7}}, + title = "{Extraction de programmes dans le Calcul des Constructions}", + type = {Th\`ese d'universit\'e}, + year = {1989}, + url = {http://www.lri.fr/~paulin/these.ps.gz}, +} + +@MASTERTHESIS{ri99, + author = "A. Ricci", + school = {{Universit\`a degli studi di Bologna}}, + title = "{Studio e progettazione di un modello RDF per biblioteche matematiche +elettroniche}", + type = {Tesi universitaria}, + year = {1999} +} + +@inproceedings{Rob65, + author="{Robinson J. A.}", + title = "{A machine-oriented logic based on the resolution principle}", + pages = "23--41", + booktitle = "Journal of the ACM", + volume = "2", + year ="1965" +} + +@inproceedings{sh:1995, + author="{Saibi A.} and {Huet G.}", + title="{Constructive Category Theory}", + booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory", + address="Goteborg (Sweden)", + month="January", + year="1995" + } + +@inproceedings{ranta2, + author="Thomas Hallgren and Aarne Ranta", + title="An extensible proof text editor", + BOOKTITLE = {LPAR'2000}, + SERIES = {LNCS/LNAI}, + VOLUME = 1955, + YEAR = 2000 + } + +@inproceedings{werner:1997, + author="Benjamin Werner", + title="{Constructive Category Theory}", + booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software", + year="1997" + } + diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex index e298dad21..8ed71abe6 100644 --- a/helm/papers/matita/matita.tex +++ b/helm/papers/matita/matita.tex @@ -43,6 +43,7 @@ \institute{Department of Computer Science, University of Bologna\\ Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY\\ \email{$\{$asperti,sacerdot,tassi,zacchiro$\}$@cs.unibo.it}} +\bibliographystyle{plain} \begin{document} \maketitle @@ -53,7 +54,7 @@ \section{Introduction} \label{sec:intro} {\em Matita} is the proof assistant under development by the \HELM{} team -\cite{annals} at the University of Bologna, under the direction of +\cite{mkm-helm} at the University of Bologna, under the direction of Prof.~Asperti. The origin of the system goes back to 1999. At the time we were mostly interested to develop tools and techniques to enhance the accessibility @@ -80,7 +81,7 @@ active in the MathML Working group since 1999, and developed inside \HELM{} a MathML-compliant widget for the GTK graphical environment which can be integrated in any application. \end{itemize} -The exportation issue, extensively discussed in \cite{exportation}, +The exportation issue, extensively discussed in \cite{exportation-module}, has several major implications worth to be discussed. The first @@ -209,7 +210,7 @@ reduce our code in sensible way).\NOTE{righe\\\COQ{}} \ASSIGNEDTO{zack} \begin{table} - \caption{\label{tab:termsyn} Concrete syntax of CIC terms in \MATITA{}.\strut} + \caption{\label{tab:termsyn} Concrete syntax of CIC terms: built-in notation\strut} \hrule \[ \begin{array}{@{}rcll@{}} @@ -254,31 +255,94 @@ reduce our code in sensible way).\NOTE{righe\\\COQ{}} \hrule \end{table} +\subsubsection{Term input} +The primary form of user interaction employed by \MATITA{} is textual script +editing: the user can modifies it and evaluate step by step its composing +\emph{statements}. Examples of statements are inductive type definitions, +theorem declarations, LCF-style tacticals, and macros (e.g. \texttt{Check} can +be used to ask the system to refine a given term and pretty print the result). +Since many statements refer to terms of the underlying calculus, \MATITA{} needs +a concrete syntax able to encode terms of the Calculus of Inductive +Constructions. +Two of the requirements in the design of such a syntax are apparently in +contrast: +\begin{enumerate} + \item the syntax should be as close as possible to common mathematical practice + and implement widespread mathematical notions; + \item each term described by the syntax should be non-ambiguous meaning that it + should exists a function which associates to each term of the syntax a CIC + term. +\end{enumerate} + +These two requirements are addressed in \MATITA{} by the mean of two mechanisms +which work together: \emph{term disambiguation} and \emph{extensible notation}. +Their interaction is visible in the architecture of the \MATITA{} input phase, +depicted in Fig.~\ref{fig:inputphase}. The architecture is articulated as a +pipline of three levels: the concrete syntax level (level 0) is the one the user +has to deal with when inserting CIC terms; the abstract syntax level (level 2) +is an internal representation which intuitively encodes mathematical formulae at +the content level \NOTE{rif. per\\ content}; the formal mathematics level (level +3) is the CIC encoding of terms. + +Requirement (1) is addressed by a built-in concrete syntax for terms, described +in Tab.~\ref{tab:termsyn}, and the extensible notation mechanisms which offers a +way for extending available mathematical notations. Extensible notation, which +is also in charge of providing a parsing function mapping concrete syntax terms +to content level terms, is described in Sect.~\ref{sec:notation}. Requirement +(2) is addressed by the conjunct action of that parsing function and +disambiguation which provides a function from content level terms to CIC terms. + +\subsubsection{Sources of ambiguity} + +The translation from content level terms to CIC terms is not straightforward +because some nodes of the content encoding admit more that one CIC encoding, +invalidating requirement (2). + +\begin{example} + + Consider the term \texttt{\TEXMACRO{forall} x. x + ln 1 = x}, the type of a + lemma the user may want to prove. Assuming that both \texttt{+} and \texttt{=} + are parsed as infix operators, all the following questions are legitimate and + must be answered before obtaining a CIC term from its content level encoding + (Fig.~\ref{fig:inputphase}(b)): + + \begin{enumerate} -The disambiguation phase builds CIC terms from ASTs of user inputs (also called -\emph{ambiguous terms}). Ambiguous terms may carry three different \emph{sources -of ambiguity}: unbound identifiers, literal numbers, and literal symbols. -\emph{Unbound identifiers} are sources of ambiguity since the same name -could have been used to represent different objects. For example, three -different theorems of the \COQ{} library share the name $\mathit{plus\_assoc}$ -(locating them is an exercise for the interested reader. Hint: use \WHELP's -\LOCATE{} query). + \item Since \texttt{ln} is an unbound identifier, which CIC constants does it + represent? Many different theorems in the library may share its (rather + short) name \dots -\emph{Numbers} are ambiguous since several different encodings of them could be -provided in logical systems. In the \COQ{} standard library for example we found -naturals (in their unary encoding), positives (binary encoding), integers -(signed positives), and reals. Finally, \emph{symbols} (instances of the -\emph{binop} and \emph{unop} syntactic categories of Table~\ref{tab:syntax}) are -ambiguous as well: infix \texttt{+} for example is overloaded to represent -addition over the four different kinds of numbers available in the \COQ{} -standard library. Note that given a term with more than one sources of -ambiguity, not all possible disambiguation choices are valid: for example, given -the input \texttt{1+1} we must choose an interpretation of \texttt{+} which is -typable in CIC according to the chosen interpretation for \texttt{1}; choosing -as \texttt{+} the addition over natural numbers and as \texttt{1} the real -number $1$ will lead to a type error. + \item Which kind of number (\IN, \IR, \dots) the \texttt{1} literal stand for? + Which encoding is used in CIC to represent it? E.g., assuming $1\in\IN$, is + it an unary or a binary encoding? + + \item Which kind of equality the ``='' node represents? Is it Leibniz's + polymorhpic equality? Is it a decidable equality over \IN, \IR, \dots? + + \end{enumerate} + +\end{example} + +In \MATITA, three \emph{sources of ambiguity} are admitted for content level +terms: unbound identifiers, literal numbers, and literal symbols. + +\emph{Unbound identifiers} (question 1) are sources of ambiguity since the same +name could have been used in the proof assistant library to represent different +objects. \emph{Numbers} (question 2) are ambiguous since several different +encodings of them could be provided in the calculus. Finally, \emph{symbols} +(question 3) are ambiguous as well, since they may be used in an overloaded +fashion to represent the application of different objects. + +\textbf{FINQUI, il resto \`e copy and paste dal Whelp paper \dots} + +Note that given a content level term with more than one sources of ambiguity, +not all possible disambiguation choices are valid: for example, given the input +\texttt{1+1} we must choose an interpretation of \texttt{+} which is typable in +CIC according to the chosen interpretation for \texttt{1}; choosing as +\texttt{+} the addition over natural numbers and as \texttt{1} the real number +$1$ will lead to a type error. A \emph{disambiguation algorithm} takes as input an ambiguous term and return a fully determined CIC term. The \emph{naive disambiguation algorithm} takes as @@ -315,7 +379,7 @@ metavariables and a refiner can be implemented. This is the case for CIC and several other logics. \emph{Metavariables}~\cite{munoz} are typed, non linear placeholders that can occur in terms; $?_i$ usually denotes the $i$-th metavariable, while $?$ denotes -a freshly created metavariable. A \emph{refiner}~\cite{mcbride} is a +a freshly created metavariable. A \emph{refiner}~\cite{McBride} is a function whose input is a term with placeholders and whose output is either a new term obtained instantiating some placeholder or $\epsilon$, meaning that no well typed instantiation could be found for the placeholders occurring in @@ -359,6 +423,7 @@ be found in~\cite{disambiguation}, where an equivalent algorithm that avoids backtracking is also presented. \subsection{notazione} +\label{sec:notation} \ASSIGNEDTO{zack} \subsection{libreria tutta visibile} @@ -406,51 +471,7 @@ the development of Matita, and in particular A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi, V.Tamburrelli. - -\begin{thebibliography}{} - - \bibitem{ida}A.Asperti, H.Geuvers, I.Loeb, L.E.Mamane, C.Sacerdoti Coen. - An Interactive Algebra Course with Formalised Proofs and Definitions. - Post-Proceedings of the Fourth International Conference on - Mathemtical Knowledge Management. Bremen, Germany, July 2005. LNCS, - to appear. - - \bibitem{annals} A.~Asperti, F.~Guidi, L.~Padovani, C.~Sacerdoti Coen, - I.~Schena. \emph{Mathematical Knowledge Management in HELM}. Annals of - Mathematics and Artificial Intelligence, 38(1): 27--46; May 2003. - - \bibitem{whelp} A.~Asperti, F.~Guidi, C.~Sacerdoti Coen, - E.Tassi, S.Zacchiroli. \emph{A content based mathematical search - engine: whelp}. Post-proceedings of the Types 2004 International - Conference, Jouy-en-Josas, France, December 2004. LNCS (to appear). - - \bibitem{metadata2} A. Asperti, M. Selmi. \emph{Efficient Retrieval of - Mathematical Statements}. In Proceeding of the Third International Conference - on Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland. LNCS 3119. - \bibitem{pechino} A.Asperti, B.Wegner. \emph{An Approach to - Machine-Understandable Representation of the Mathematical Information in - Digital Documents}. In: Fengshai Bai and Bernd Wegner (eds.): Electronic - Information and Communication in Mathematics, LNCS vol. 2730, - pp. 14--23, 2003 - - \bibitem{coq} The Coq proof-assistant, \url{http://coq.inria.fr} - - \bibitem{metadata1} F. Guidi, C. Sacerdoti Coen. \emph{Querying Distributed - Digital Libraries of Mathematics}. In Proceedings of Calculemus 2003, 11th - Symposium on the Integration of Symbolic Computation and Mechanized - Reasoning. Aracne Editrice. - - \bibitem{exportation} C. Sacerdoti Coen. \emph{From Proof-Assistans to - Distributed Libraries of Mathematics: Tips and Pitfalls}. - In Proc. Mathematical Knowledge Management 2003, Lecture Notes in Computer - Science, Vol. 2594, pp. 30--44, Springer-Verlag. - - \bibitem{disambiguation} C. Sacerdoti Coen, S. Zacchiroli. \emph{Efficient - Ambiguous Parsing of Mathematical Formulae}. In Proceedings of the Third - International Conference on Mathematical Knowledge Management, MKM 2004. - LNCS,3119. - -\end{thebibliography} +\bibliography{matita} \end{document} -- 2.39.2