--- /dev/null
+
+@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"
+ }
+
projects / helm.git / commitdiff