2 @inproceedings{latexmathml,
3 author = {Luca Padovani},
4 title = {On the Roles of LATEX and MathML in Encoding and Processing Mathematical Expressions},
5 booktitle = {MKM '03: Proceedings of the Second International Conference on Mathematical Knowledge Management},
7 isbn = {3-540-00568-4},
9 publisher = {Springer-Verlag},
10 address = {London, UK},
13 @inproceedings{gmetadom,
14 author = "Luca Padovani and Claudio Sacerdoti Coen and Stefano Zacchiroli",
15 title = "A Generative Approach to the Implementation of Language Bindings for the Document Object Model",
16 booktitle = "Generative Programming and Component Engineering",
17 editor = "Gabor Karsai and Eelco Visser",
21 publisher = "Springer-Verlag",
26 author = "Freek Wiedijk",
27 title = "MMode, a Mizar Mode for the proof assistant Coq",
28 institution = "University of Nijmegen",
29 number = "NIII-R0333",
33 @article{ lamport-proof,
34 author = "Leslie Lamport",
35 title = "How to write a proof",
36 journal = "American Mathematical Monthly",
43 @inproceedings{thery-authoring,
44 author = "Laurent Th\`ery",
45 title = "Formal Proof Authoring: an Experiment",
46 booktitle = "User Interface Design for Theorem Provers",
47 editor = "David Aspinall and Christoph L{\"u}th",
51 @inproceedings{padovani-editex,
52 author = "Luca Padovani",
53 title = "Interactive Editing of MathML Markup Using TeX Syntax",
54 booktitle = "International Conference on TeX, XML, and Digital Typography",
59 publisher = "Springer-Verlag",
62 @inproceedings{uitp-knowledge-modelling,
63 author = "Stuart Aitken",
64 title = "Problem Solving in Interactive Proof: A Knowledge-Modelling Approach",
65 booktitle = "European Conference on Artificial Intelligence (ECAI)",
69 @inproceedings{proof-by-pointing,
70 author = "Yves Bertot",
71 title = "Proof by Pointing",
72 booktitle = "Symposium on Theoretical Aspects Computer Software (STACS)",
73 series = "Lecture Notes in Computer Science",
78 @inproceedings{thery-cyp,
79 author = "Laurent Th\`ery",
80 title = "Colouring proofs: a lightweight approach to adding formal structure to proofs",
81 booktitle = "User Interface Design for Theorem Provers",
82 editor = "David Aspinall and Christoph L{\"u}th",
86 @article{uitp-empirical,
87 author = "Stuart Aitken and Phil Gray and Tom Melham and Muffy Thomas",
88 title = "Interactive Theorem Proving: An Empirical Study of User Activity",
89 journal = "Journal of Symbolic Computation",
93 @inproceedings{uitp-phases,
94 author = "Stuart Aitken and Phil Gray and Tom Melham and Muffy Thomas",
95 title = "Phases, Modes and Information Flow in Theory Development",
96 booktitle = "User Interface Design for Theorem Provers",
97 editor = "Nicholas Merriam",
101 @inproceedings{searchingmath,
102 author = "Andrea Asperti and Stefano Zacchiroli",
103 title = "Searching mathematics on the Web: state of the art and future developments",
104 booktitle = "New Developments in Electronic Publishing of Mathematics",
105 editor = "Bernd Wegner",
106 publisher = {FIZ Karlsruhe},
111 author = "K. Appel and W. Haken",
112 title = "Every planar map is four colorable.",
113 journal = {Illinois Journal of Mathematics},
119 @misc{freekcomparison,
120 author = "Freek Wiedijk",
121 title = "The Sixteen Provers of the World",
122 howpublished = "University of Nijmegen,\\\url{http://www.cs.ru.nl/~freek/comparison/comparison.ps.gz}"
126 title = "Zentralblatt MATH",
127 howpublished = "\url{http://www.emis.de/ZMATH/}"
131 author = "Michael J. C. Gordon and Robin Milner and C.P. Wadsworth",
132 title = "{Edinburgh LCF}: a Mechanised Logic of Computation",
133 series = {Lecture Notes in Computer Science},
135 publisher = {{Sprin\-ger-Verlag}},
140 author = "Claudio Sacerdoti Coen",
141 title = "Mathematical Knowledge Management and Interactive Theorem
143 school = "University of Bologna",
145 note = "Technical Report UBLCS 2004-5"
149 author = "Markus Wenzel",
150 title = "Isar - A Generic Interpretative Approach to Readable Formal Proof Documents",
151 booktitle = "Theorem Proving in Higher Order Logics",
156 @inproceedings{centaur,
157 author = "P. Borras and D. Clement and Th. Despeyrouz and J. Incerpi and G. Kahn and B. Lang and V. Pascual",
158 title = "{CENTAUR}: The System",
159 booktitle = "Proceedings of the {ACM} {SIGSOFT}/{SIGPLAN} Software Engineering Symposium on Practical Software Development Environments ({PSDE})",
160 journal = "SIGPLAN Notices",
163 publisher = "ACM Press",
164 address = "New York, NY",
167 url = "citeseer.nj.nec.com/borras88centaur.html"
170 @inproceedings{Leroy-manifest-types,
171 AUTHOR = "Xavier Leroy",
172 TITLE = "Manifest types, modules, and separate compilation",
173 BOOKTITLE = {21st symposium Principles of Programming Languages},
175 PUBLISHER = {ACM Press},
177 URL = {http://pauillac.inria.fr/~xleroy/publi/manifest-types-popl.ps.gz}
180 @inproceedings{overkilling,
181 author = "Sacerdoti Coen, Claudio",
182 title = "Tactics in Modern Proof-Assistants: the Bad Habit of
184 booktitle = "Supplementary Proceedings of the 14th International
185 Conference TPHOLS 2001",
190 @inproceedings{omegaants1,
191 author = "Christoph Benzm{\"u}ller and Volker Sorge",
192 title = {{OANTS} -- An open approach at combining Interactive and Automated
194 booktitle = {Symbolic Computation and Automated Reasoning},
195 editor = {Manfred Kerber and Michael Kohlhase},
198 publisher = {A.K.Peters},
199 url = {www.ags.uni-sb.de/~chris/papers/C8.pdf}
203 author = "R. Fateman and T. Tokuyasu and B. Berman and N. Mitchell",
204 title = {Optical Character Recognition and Parsing of Typeset Mathematics},
205 journal = {Journal of Visual Communication And Image Representation},
211 url = {www.ags.uni-sb.de/~chris/papers/J4.pdf}
214 @article{newauthomath,
215 author = "Freek Wiedijk",
216 title = "A new implementation of {A}utomath",
217 journal = {Journal of Automated Reasoning},
224 author = "Paolo Casarini and Luca Padovani",
225 title = "The {G}nome {DOM} {E}ngine",
226 journal = "Markup Languages: Theory \& Practice",
231 publisher = "MIT Press",
236 author = "Christoph Benzm{\"u}ller and Mateja Jamnik and Manfred Kerber and
238 title = {Agent based Mathematical Reasoning},
239 journal = {Electronic Notes in Theoretical Computer Science, Elsevier},
244 url = {www.ags.uni-sb.de/~chris/papers/J4.pdf}
247 @inproceedings{Necula,
248 author = "George C. Necula and Peter Lee",
249 title = "Safe Kernel Extensions Without Run-Time Checking",
250 booktitle = "2nd Symposium on Operating Systems Design and Implementation ({OSDI} '96), October 28--31, 1996. Seattle, {WA}",
251 publisher = "USENIX",
252 address = "Berkeley, CA, USA",
256 url = "citeseer.nj.nec.com/necula96safe.html"
259 @inproceedings{courant,
260 AUTHOR = "Judica{\"e}l Courant",
261 TITLE = {Explicit Universes for the {C}alculus of {C}onstructions},
262 BOOKTITLE = {Theorem Proving in Higher Order Logics:
263 15th International Conference, TPHOLs 2002},
264 EDITOR = {Victor A. {Carre\~{n}o} and C\'{e}sar A. {Mu\~{n}oz} and Sofi\`{e}ne Tahar},
265 SERIES = {Lecture Notes in Computer Science},
269 PUBLISHER = {{Sprin\-ger-Verlag}},
271 ADDRESS = {Hampton, VA, USA}
275 author = "George C. Necula and Peter Lee",
276 title="{Efficient Representation and Validation of Proofs}",
277 booktitle="Proceedings of the 13th Annual symposium on Logic in Computer Science,",
278 address="Indianapolis",
283 author = "Jean-Yves Girard and Yves Lafont and Paul Taylor",
284 title = "{Proofs and Types}",
285 publisher = {Cambridge University Press},
286 series = {Cambridge Tracts in Theoretical Computer Science},
290 @inproceedings{proofgeneral,
291 author = "David Aspinall",
292 title = "{P}roof {G}eneral: A Generic Tool for Proof Development",
293 booktitle = "Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000",
298 publisher = "Springer-Verlag",
301 @inproceedings{Gim94,
302 author = "Eduardo Gim\'enez",
303 title = "{Codifying guarded definitions with recursive schemes}",
304 booktitle = "Types'94: Types for Proofs and Programs",
308 publisher = "Springer-Verlag",
309 note = "Extended version in LIP research report 95-07, ENS Lyon",
313 @incollection{BarendregtH:lawcwt,
314 author = "H. Barendregt",
315 title = "{Lambda Calculi with Types}",
316 booktitle = "{Handbook of Logic in Computer Science}",
317 editor = "{Abramsky, Samson and others}",
318 publisher = "{Oxford University Press}",
323 @inproceedings{coquand:1986,
324 author="Thierry Coquand",
325 title="{An Analysis of Girard's Paradox}",
326 booktitle="Symposium on Logic in Computer Science",
328 publisher="MA. IEEE press",
333 AUTHOR = "Christine Paulin-Mohring",
334 TITLE = {D\'efinitions Inductives en Th\'eorie des Types d'Ordre Sup\'rieur},
335 SCHOOL = {Universit\'e Claude Bernard Lyon I},
338 TYPE = {Habilitation \`a diriger les recherches},
339 URL = {http://www.lri.fr/~paulin/habilitation.ps.gz}
343 author = "Jacques Garrigue",
344 title = "{Label-Selective Lambda-Calculi and Transformation Calculi}",
345 school = "University of Tokyo, Department of Information Science",
350 @phdthesis{LuoZ:extcc,
351 author = "Zhaohui Luo",
352 title = "{An Extended Calculus of Constructions}",
353 school = "University of Edinburgh",
358 author = "Laurent Chicli",
359 title = "Sur la formalisation des math\'ematiques dans le
360 {C}alcul des {C}onstructions {I}nductives",
361 school = "Universit\'e de Nice~-~Sophia Antipolis",
365 @phdthesis{geuvers:1993,
366 author="Herman Geuvers",
367 title="{Logics and Type Systems}",
368 school="Catholic University Nijmegen",
370 type="{Ph.D.} dissertation"
373 @unpublished{PrimesInP,
374 author = "M. Agrawal and N. Kayal and N. Saxena",
375 title = "{PRIMES} in {P}",
376 note = "\url{http://www.cse.iitk.ac.in/users/manindra/primality.ps}",
381 @unpublished{danosKAM,
382 author = "Vincent Danos and Laurent Regnier",
383 title = "How abstract machines implement head linear reduction",
387 @inproceedings{Oostdijk,
388 author = "Olga Caprotti and Herman Geuvers and Martin Oostdijk",
389 title = "Certified and Portable Mathematical Documents from Formal Contexts",
390 editor = "Bruno Buchberger and Olga Caprotti",
391 booktitle = "On-Line Proceedings of the First International Conference on
392 Mathematical Knowledge Management, MKM 2001",
393 publisher = "The Electronic Library of Mathematics (EMIS)",
394 url = "\url{http://www.emis.de/ELibM.html}",
398 @inproceedings{formal-proof-sketches,
399 author = "Freek Wiedijk",
400 title = "Formal Proof Sketches",
401 editor = "Wan Fokkink and Jaco van de Pol",
402 booktitle = "7th Dutch Proof Tools Day, Program + Proceedings",
403 note = "CWI, Amsterdam",
407 @inproceedings{Barendregt,
408 author = "Henk Barendregt",
409 title = "Towards an Interactive Mathematical Proof Language",
410 editor = "Fairouz Kamareddine",
411 booktitle = "Thirty Five Years of Automath",
413 publisher = "Kluwer",
417 @inproceedings{werner:prof-irrelevance,
418 author = "Alexandre Miquel and Benjamin Werner",
419 title = "The Not So Simple Proof-Irrelevant Model of {CC}",
420 editor = "Herman Geuvers and Freek Wiedijk",
421 booktitle = "Types for Proofs and Programs: International Workshop, TYPES 2002",
423 volume = "LNCS, 2646",
424 publisher = "Springer-Verlag",
428 @inproceedings{csc-environment,
429 author = "Claudio Sacerdoti Coen",
430 title = "Mathematical Libraries as Proof Assistant Environments",
431 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
432 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
433 volume = "LNCS, 3119",
435 publisher = "Springer-Verlag",
439 @inproceedings{disambiguation,
440 author = "Claudio Sacerdoti Coen and Stefano Zacchiroli",
441 title = "Efficient Ambiguous Parsing of Mathematical Formulae",
442 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
443 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
444 volume = "LNCS, 3119",
446 publisher = "Springer-Verlag",
450 @inproceedings{pechino,
451 author = "Andrea Asperti and Bernd Wegner",
452 title = "An Approach to Machine-Understandable Representation of the Mathematical Information in Digital Documents",
453 editor = "Fengshai Bai and Bernd Wegner",
454 booktitle = "Electronic Information and Communication in Mathematics",
455 volume = "LNCS, 2730",
457 publisher = "Springer-Verlag",
461 @inproceedings{whelp,
462 author = "Andrea Asperti and Ferruccio Guidi and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli",
463 title = "A content based mathematical search engine: Whelp",
464 booktitle = "Post-proceedings of the Types 2004 International Conference",
465 volume = "LNCS, (to appear)",
467 publisher = "Springer-Verlag",
471 @inproceedings{exportation-module,
472 author = "Sacerdoti Coen, Claudio",
473 title = "From Proof-Assistans to Distributed Libraries of Mathematics: Tips
475 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
476 booktitle = "Proceedings of the Second International Conference on
477 Mathematical Knowledge Management, MKM 2003",
479 volume = "LNCS, 2594",
480 publisher = "Springer-Verlag",
485 author = "Andrea Asperti and Herman Geuvers and Iris Loeb and Lionel Elie Mamane and Claudio Sacerdoti Coen",
486 title = "An Interactive Algebra Course with Formalised Proofs and Definitions",
487 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
488 booktitle = "Post-Proceedings of the Fourth International Conference on Mathematical Knowledge Management, MKM 2005",
490 volume = "LNCS, (to appear)",
491 publisher = "Springer-Verlag",
495 @inproceedings{davenport,
496 author = "James H. Davenport",
497 title = "{MKM} from Book to Computer: A Case Study",
498 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
499 booktitle = "Proceedings of the Second International Conference on
500 Mathematical Knowledge Management, MKM 2003",
502 volume = "LNCS, 2594",
503 publisher = "Springer-Verlag",
507 @inproceedings{fguidisacerdot,
508 author = "Ferruccio Guidi and Sacerdoti Coen, Claudio",
509 title = "Querying Distributed Digital Libraries of Mathematics",
510 editor = "Therese Hardin and Renaud Rioboo",
511 booktitle = "Calculemus 2003",
513 publisher = "Aracne Editrice S.R.L.",
515 note = "ISBN 88-7999-545-6"
518 @inproceedings{hbugs,
519 author = "Sacerdoti Coen, Claudio and Stefano Zacchiroli",
520 title = "Brokers and {W}eb-Services for Automatic Deduction: a Case Study",
521 editor = "Therese Hardin and Renaud Rioboo",
522 booktitle = "Calculemus 2003",
524 publisher = "Aracne Editrice S.R.L.",
526 note = "ISBN 88-7999-545-6"
529 @inproceedings{calculemus-presentation,
530 author = "Christoph Benzm{\"u}ller",
531 title = "The {CALCULEMUS} Research Training Network -- A short Overview",
532 editor = "Therese Hardin and Renaud Rioboo",
533 booktitle = "Calculemus 2003",
535 publisher = "Aracne Editrice S.R.L.",
537 note = "ISBN 88-7999-545-6"
540 @inproceedings{linda,
541 author = "Sacerdoti Coen, Claudio",
542 title = "A Constructive Proof of the Soundness of the
543 Encoding of Random Access Machines in a Linda Calculus with Ordered
545 booktitle = "Theoretical Computer Science: 8th Italian Conference, ICTCS 2003",
547 volume = "LNCS, 2841",
548 publisher = "Springer-Verlag",
552 @article{asperti-categorical-understanding,
553 author = "Andrea Asperti",
554 title = "A categorical understanding of environment machines",
555 journal = "Journal of Functional Programming",
563 @article{namelessdummies,
564 author = "{N. G. de Bruijn}",
565 title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem",
566 journal = "Indagationes Mathematicae",
573 author = "Yves Bertot",
574 title = "The CtCoq System: Design and Architecture",
575 journal = "Formal Aspects of Computing",
582 author = "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
583 title = "Real Theorem Provers Deserve Real User-Interfaces",
586 institution = "INRIA",
587 number = "{Inria Research Report 1684}"
591 author = "Yves Bertot and Laurent Th\'ery",
592 title = "A Generic Approach to Building User Interfaces for Theorem Provers",
593 journal = "Journal of Symbolic Computation",
600 author = "Michael Kohlhase and Andreas Franke",
601 title = "{MBase}: Representing Knowledge and Context for the Integration of Mathematical Software Systems",
602 journal = "Journal of Symbolic Computation",
607 url = "\url{http://citeseer.nj.nec.com/kohlhase00mbase.html}"
610 @inproceedings{mizarql,
611 author = "Grzegorz Bancerek and Piotr Rudnicki",
612 title = "Information Retrieval in {MML}",
613 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
614 booktitle = "Proceedings of the Second International Conference on
615 Mathematical Knowledge Management, MKM 2003",
617 volume = "LNCS, 2594",
618 publisher = "Springer-Verlag",
622 @article{codedcontexttrees,
623 author = "Harald Ganzinger and Robert Nieuwehuis and Pilar Nivela",
624 title = "Fast Term Indexing with Coded Context Trees. Journal of Automated Reasoning",
625 journal = "Journal of Automated Reasoning",
630 author = "Aarne Ranta",
631 title = "Grammatical Framework: A Type-Theoretical Grammar Formalism",
632 journal = "Journal of Functional Programming",
634 note = "Manuscript made available in September 2002"
638 AUTHOR = "Di Cosmo, Roberto",
639 TITLE = {Isomorphisms of types: from $\lambda$-calculus to information retrieval and language design},
640 SERIES = {Progress in Theoretical Computer Science},
641 PUBLISHER = {Birkhauser},
643 NOTE = {ISBN-0-8176-3763-X}
647 EDITOR = "R.P. Nederpelt and J.H. Geuvers and R.C. de Vrijer",
648 TITLE = {Selected Papers on Automath},
649 SERIES = {Studies in Logic and the Foundations of Mathematics},
650 PUBLISHER = {Elsevier Science},
653 NOTE = {ISBN-0444898220}
657 author = "Jean-Louis Krivine",
658 title = "Un interpr\`ete du $\lambda$-calcul",
659 howpublished = "Brouillon. Available on-line at \url{http://www.logique.jussieu.fr/~krivine}",
664 title = "Progress Report: Building Interactive Digital Libraries of Formal
665 Algorithmic Knowledge",
666 howpublished = "Cornell University, \url{http://www.cs.uwyo.edu/~nuprl/documents/cornell_slides.pdf}",
672 @misc{metadata4education,
673 title = "{L}earning {O}bject {M}etadata Standard",
674 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+",
679 @misc{openmath-cd-with-plus,
680 title = "Arith1 {OpenMath} {C}ontent {D}ictionary",
681 howpublished = "The OpenMath Society, \url{http://www.openmath.org/cocoon/openmath/cd/arith1.ocd}",
683 key = "Arith1 OpenMath Content Dictionary"
688 title = "Dewey Decimal Classification",
689 howpublished = "\url{http://www.oclc.org/dewey}",
690 url = "\url{http://www.oclc.org/dewey}",
695 title = "Library of Congress Classification Scheme",
696 howpublished = "\url{http://www.loc.gov}",
697 url = "\url{http://www.loc.gov}",
702 title = "Mathematical {S}ubject {C}lassification, {A}merican {M}athematical {S}ociety",
703 howpublished = "\url{http://www.ams.org/msc}",
704 url = "\url{http://www.ams.org/msc}",
708 @InCollection{borges,
709 author = "Jorge Luis Borges",
710 title = "The Library of {B}abel",
711 publisher = "Grove Press",
712 booktitle = "Ficciones",
716 @inproceedings{magaud,
717 author = "Nicolas Magaud",
718 title = "{C}hanging {D}ata {R}epresentation within the {C}oq {S}ystem",
719 booktitle = {TPHOLs'2003},
720 publisher = {Springer-Verlag},
721 volume = {LNCS, 2758},
725 @inproceedings{geuvers-jojgov,
726 author = "Herman Geuvers and Gueorgui I. Jojgov",
727 title = "Open Proofs and Open Terms: A Basis for Interactive Logic",
728 editor = "J. Bradfield",
729 booktitle = "Computer Science Logic: 16th International Workshop, CLS 2002",
731 volume = "LNCS, 2471",
732 publisher = "Springer-Verlag",
737 @inproceedings{mkm-structure,
738 author = "Koji Nakagawa and Akihiro Nomura and Masakazu Suzuki",
739 title = "Extraction of Logical Structure from articles in Mathematics",
740 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
741 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
742 volume = "LNCS, 3119",
744 publisher = "Springer-Verlag",
748 @inproceedings{mkm-metadata2,
749 author = "Andrea Asperti and Matteo Selmi",
750 title = "Efficient Retrieval of Mathematical Statements",
751 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
752 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
753 volume = "LNCS, 3119",
755 publisher = "Springer-Verlag",
759 @inproceedings{adams,
760 author = "A. A. Adams",
761 title = "Digitisation, Representation and Formalisation: Digital
762 Libraries of Mathematics.",
763 editor = "A. Asperti, B. Buchberger, J.H. Davenport",
764 booktitle = "Proceedings of Mathematical Knowledge Management 2003",
765 volume = "LNCS, 2594",
767 publisher = "Springer-Verlag",
772 author = "Serge Autexier and Dieter Hutter and Heiko Mantel and Axel Schairer",
773 title = "Towards an Evolutionary Formal Software-Development Using {CASL}",
774 booktitle = "WADT99 Selected Papers Volume",
775 volume = "LNCS, 1827",
776 publisher = "Springer-Verlag",
780 @inproceedings{how-to-extract,
781 author = "Lu\'is Cruz Filipe and Bas Spitters",
782 title = "Program Extraction from large proof developments",
783 booktitle = "Proceedings of TPHOLS 2003",
784 editor = "D. Basin and B. Wolff",
785 volume = "LNCS, 2758",
786 publisher = "Springer-Verlag",
790 @inproceedings{click-and-prove,
791 author = "Jean-Raymond Abrial and Dominique Cansell",
792 title = "Click'n {P}rove: Interactive Proofs Within Set Theory",
793 booktitle = "Proceedings of TPHOLS 2003",
794 editor = "D. Basin and B. Wolff",
795 volume = "LNCS, 2758",
796 publisher = "Springer-Verlag",
800 @inproceedings{delahaye,
801 author = "David Delahaye and Roberto di Cosmo",
802 title = "Information Retrieval in a {C}oq Proof Library using
804 booktitle = "Proceedings of TYPES 99",
806 publisher = "Springer-Verlag",
811 author = "G. I. Jojgov",
812 title = "Systems for open terms: An Overview",
813 institution = "Technische Universiteit Eindhoven",
814 number = "CSR 01-03",
818 @TechReport{garrigue:implicit-arguments,
819 author = "Jun P. Furuse and Jacques Garrigue",
820 title = " A label-selective lambda-calculus with optional arguments and its compilation method",
821 institution = "Research Institute for Mathematical Sciences, Kyoto University",
822 number = "RIMS Preprint 1041",
828 author = "Alexandre Miquel",
829 title = "Le {C}alcul des {C}onstructions {I}mplicite: syntaxe et s\'emantique",
830 school = "Universit\'e Paris 7",
834 @phdthesis{chrzaszcz,
835 author = "Jacek Chrz{\c{a}}szcs",
836 title = "Modules in Type Theory with Generative Definitions",
837 school = "Uniwersytet Warszawski and Universit\'e de Paris Sud",
842 author = "Olivier Pons",
843 title = "Conception et r\'ealisation d'outils d'aide au d\'eveloppement de grosse th\'eories dans les syst\`emes de preuves interactifs",
844 school = "Conservatoire National des Arts et M\'etiers",
849 author = "Fr\'ed\'eric Blanqui",
850 title = "Type Theory and Rewriting",
851 school = "Universit\'e Paris XI",
855 @phdthesis{magnusson,
856 author = "Lena Magnusson",
857 title = "The Implementation of {ALF} -- a Proof Editor based
858 on Martin-L{\"o}f Monomorphic Type Theory with Explicit
860 school = "Chalmers University of Technology / G{\"o}teborg University",
865 author = "Conor McBride",
866 title = "Dependently Typed Functional Programs and their Proofs",
867 school = "University of Edinburgh",
872 author = "Irene Schena",
873 title = "Towards a Semantic Web for Formal Mathematics",
874 school = "University of Bologna",
879 author = "Ferruccio Guidi",
880 title = "Searching and Retrieving in Content-Based Repositories
881 of Formal Mathematical Knowledge",
882 school = "University of Bologna",
885 note = "Technical Report UBLCS 2003-06"
889 author = "Luca Padovani",
890 title = "MathML Formatting",
891 school = "University of Bologna",
894 note = "Technical Report UBLCS 2003-03"
897 @mastersthesis{csc-master,
898 author = "Sacerdoti Coen, Claudio",
899 title = "Progettazione e realizzazione con tecnologia {XML} di basi distribuite di conoscenza matematica formalizzata",
900 school = "University of Bologna",
904 @mastersthesis{zack-master,
905 author = "Stefano Zacchiroli",
906 title = "Web {s}ervices per il supporto alla dimostrazione interattiva",
907 school = "University of Bologna",
911 @mastersthesis{dilena,
912 author = "Pietro Dilena",
913 title = "Generazione automatica di stylesheet per notazione matematica",
914 school = "University of Bologna",
919 author = "C\'esar Munoz",
920 title = "A Calculus of Substitutions for Incomplete-Proof
921 Representation in Type Theory",
928 author = "Martin Strecker",
929 title = "Construction and Deduction in Type Theories",
930 school = "Universit{\"a}t Ulm",
934 @misc{content-centric,
935 author = "Andrea Asperti and Luca padovani and Claudio Sacerdoti Coen
937 title = "Content-centric Logical Envirnoments",
938 howpublished = "Short Presentation at the Fifteenth IEEE Symposium on Logic in Computer Science",
941 key = "content centric"
944 @misc{mowgli-proposal,
945 title = "The {MoWGLI Proposal}, {HTML} Version",
946 howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/project.html}",
947 key = "MoWGLI Proposal"
950 @misc{debrujinfactor,
951 title = "The ``de Bruijn factor''",
952 howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}",
953 author = "Freek Wiedijk",
956 @misc{mowgli-deliverables,
957 title = "{MoWGLI} Project Deliverables",
958 howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html}",
959 key = "MoWGLI Deliverables"
963 title = "The {ALF} family of proof-assistants",
964 howpublished = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
965 url = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
970 title = "The {C}oq Proof Assistant Reference Manual",
971 author = "The Coq Development Team",
972 howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
977 title = "The {C}oq proof-assistant",
978 howpublished = "\\\url{http://coq.inria.fr}",
983 title = "The {PhoX} proof-assistant",
984 howpublished = "\\\url{http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html}",
989 title = "The {L}ego proof-assistant",
990 howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}",
991 url = "\url{http://www.dcs.ed.ac.uk/home/lego/}",
996 title = "The {A}lfa proof editor",
997 howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
998 url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
1003 title = "The {PVS} Specification and Verification System",
1004 howpublished = "\\\url{http://pvs.csl.sri.com/}",
1009 title = "The {Isabelle} proof-assistant",
1010 howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}",
1015 author = "Constable, Robert L. and Stuart F. Allen and H. M. Bromley and
1016 W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and
1017 T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
1019 title = "Implementing Mathematics with the {N}uprl Development System",
1020 publisher = "Prentice-Hall",
1026 title = "The {NuPRL} proof-assistant",
1027 howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
1032 title = "The {HOL Light} proof-assistant",
1033 howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}",
1038 title = "The {MONET} project",
1039 howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}",
1044 title = "The {CALCULEMUS} project",
1045 howpublished = "\url{http://www.calculemus.net/}",
1046 url = "\url{http://www.calculemus.net/}",
1051 title = "The {M}izar proof-assistant",
1052 howpublished = "\\\url{http://mizar.uwb.edu.pl/}",
1057 howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium",
1058 author = "O. Caprotti and D. P. Carlisle and A. M. Cohen",
1059 title = "{\emph{The {O}pen{M}ath {S}tandard}}"
1063 title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
1064 editor="{Patrick Ion} and others",
1065 howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
1066 url = "\url{http://www.w3.org/TR/MathML2}",
1067 key = "Mathematical"
1071 title = "{E}xtensible {M}arkup {L}anguage ({XML}). {V}ersion 1.0.",
1072 editor="{Tim Bray} and others",
1073 howpublished = "W3C Recommendation 10 February 1998,
1074 \url{http://www.w3.org/TR/REC-xml}",
1075 url = "\url{http://www.w3.org/TR/REC-xml}",
1080 title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0",
1081 howpublished = "W3C Candidate Recommendation 10 May 2000,
1082 \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1083 url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1088 title = "Universal Resource Identifiers in {WWW}",
1089 howpublished = "RFC 1630, CERN",
1096 title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0",
1097 howpublished = "W3C Recommendation, 16 November 1999,
1098 \url{http://www.w3.org/TR/xpath}",
1099 url = "\url{http://www.w3.org/TR/xpath}",
1104 title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0",
1105 howpublished = "W3C Recommendation, 16 November 1999,
1106 \url{http://www.w3.org/TR/xslt}",
1107 url = "\url{http://www.w3.org/TR/xslt}",
1112 title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax
1114 howpublished = "W3C Recommendation 22 February 1999,
1115 \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1116 url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1121 title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)",
1122 howpublished = "\\\url{http://www.mathweb.org/omdoc/omdoc.ps}",
1127 title = "The {F}ormavie project",
1128 howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1129 url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1134 title = "The {HELM} project",
1135 howpublished = "\url{http://helm.cs.unibo.it}",
1136 url = "\url{http://helm.cs.unibo.it}",
1141 title = "The {HELM} On-Line Library",
1142 howpublished = "\url{http://helm.cs.unibo.it/library.html}",
1143 url = "\url{http://helm.cs.unibo.it/library.html}",
1144 key = "HELM Library"
1148 title = "The {M}ath{W}eb project",
1149 howpublished = "\url{http://www.mathweb.org}",
1150 url = "\url{http://www.mathweb.org}",
1155 title = "The {PC}oq project",
1156 howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1157 url = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1162 author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen
1164 title = "Towards a library of formal mathematics",
1166 note = "Panel session of the 13th {I}nternation {C}onference on
1167 {T}heorem {P}roving in {H}igher {O}rder {L}ogics
1168 ({TPHOLS}'2000), Portland, Oregon, USA",
1171 @inproceedings{Ring,
1172 author = "Samuel Boutin",
1173 title = "Using Reflection to Build Efficient and Certified Decision
1175 editor = "Martin Abadi and Takahashi Ito editors",
1176 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1179 publisher = "Springer-Verlag",
1183 @inproceedings{werner-zfc,
1184 author = "Benjamin Werner",
1185 title = "Sets in Types, Types in Sets",
1186 editor = "Martin Abadi and Takahashi Ito editors",
1187 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1190 publisher = "Springer-Verlag",
1195 author = "Peter Aczel",
1196 title = "On Relating Type Theories and Set Theories",
1197 journal = "Lecture Notes in Computer Science",
1202 @inproceedings{remathematization,
1203 author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1204 title = "{XML}, Stylesheets and the re-mathematization of Formal Content",
1205 booktitle = "EXTREME",
1210 @phdthesis{YANNTHESIS,
1211 author = "Yann Coscoy",
1212 title = "Explication textuelle de preuves pour le {C}alcul des
1213 {C}onstructions {I}nductives",
1214 school = "Universit\'e de Nice-Sophia Antipolis",
1219 author = "Sylvain Lippi",
1220 title = "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)",
1221 school = "Universit\'e Aix-Marseille 2",
1226 author = "Benjamin Werner",
1227 title = "Une Th\'eorie des {C}onstructions {I}nductives",
1228 school = "Universit\'e Paris VII",
1233 @InCollection{Felleisen87,
1234 author = "M. Felleisen and D. Friedman",
1235 editor = "M. Wirsing",
1236 title = "Control operators, the {SECD}-machine, and the lambda calculus",
1237 booktitle = "Formal Description of Programming Concepts III",
1239 publisher = "Elsevier Science Publishers B.V.",
1240 address = "(North-Holland) Amsterdam",
1245 author = "Jan Zwanenburg",
1246 institution = "Eindhoven University of Technology",
1247 number = "Computing Science Report CS-98-11",
1248 title = "The Proof-assistant Yarrow",
1252 @TechReport{Ager2003a,
1253 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1254 institution = "BRICS",
1256 number = "BRICS RS-03-13",
1257 title = "A Functional Correspondence between Evaluators and Abstract Machines",
1261 @TechReport{Ager2003b,
1262 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1263 institution = "BRICS",
1265 number = "BRICS RS-03-14",
1266 title = "From Interpreter to Compiler and Virtual Machine: A Functional Derivation",
1270 @article{harperpollack,
1271 author = "Robert Harper and Robert Pollack",
1272 title = "Type checking with universes",
1273 journal = "Theoretical Computer Science",
1279 @article{activemath,
1280 author = "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich",
1281 title = "Knowledge Representation and Management in {ActiveMath}",
1282 journal = "Annals of Mathematics and Artificial Intelligence",
1290 author = "Andrea Asperti and Ferruccio Guidi and Luca Padovani and
1291 Claudio Sacerdoti Coen and Irene Schena",
1292 title = "Mathematical Knowledge Management in {HELM}",
1293 journal = "Annals of Mathematics and Artificial Intelligence",
1300 @unpublished{formal-topology,
1301 author = "Giovanni Sambin",
1302 title = "Some points in formal topology",
1303 note = "To appear in Theoretical Computer Science",
1307 @TechReport{JohnHarrison:complexity-of-floating-point-proofs,
1308 author = "John Harrison",
1309 title = "Real Numbers in Real Applications",
1310 note = "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002",
1311 institution = "NASA",
1312 number = "NASA/CP-2002-211736",
1316 @inproceedings{kohlhase-anghelache,
1317 author = "Michael Kohlhase and Romeo Anghelache",
1318 title = "Towards Collaborative Content Management And Version Control For
1319 Structured Mathematical Knowledge",
1320 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
1321 booktitle = "Proceedings of the Second International Conference on
1322 Mathematical Knowledge Management, MKM 2003",
1324 volume = "LNCS, 2594",
1325 publisher = "Springer-Verlag",
1329 %%% Unused entries from my Master dissertation bibliography
1332 title="{Standard Generalized Markup Language (SGML)}",
1333 note="ISO 8879:1986",
1338 author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1339 title = "{Content Centric Logical Environments}",
1340 note = "Short Presentation at LICS 2000",
1341 ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz",
1345 author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1346 title = "{Formal Mathematics in MathML}",
1347 note = "To be presented at MathML International Conference 2000",
1351 author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1352 title = "{Towards a Library of Formal Mathematics}",
1353 note = "Accepted at TPHOLS 2000",
1354 ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz",
1357 @techreport{mowgli:D4a,
1358 author = "Hanane Naciri and Luca Padovani",
1359 title = "{MathML} Rendering/Browsing Engine",
1360 type = {MoWGLI Report},
1363 howpublished = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}"
1366 @techreport{hazewinkel,
1367 author = "Michiel Hazewinkel",
1368 title = "Dynamic stochastic models for indexes and thesauri,
1369 identification clouds, and information retrieval and
1371 type = "{MKM Net Report}",
1372 howpublished = "\url{http://monet.nag.co.uk/mkm//index.html}"
1375 @techreport{BarrasB:coqpar,
1376 author = "{Barras B.} and {Boutin S.} and {Cornes C.}
1377 and {Courant J.} and {Filliatre J. C.}
1378 and {Gim\'enez E.} and {Herbelin H.} and {Huet G.}
1379 and {Munoz C.} and {Murthy C.} and {Parent C.}
1380 and {Paulin-Mohring C.} and {Saibi A.}
1382 title = "{The Coq Proof Assistant Reference Manual : Version
1384 institution = {Inria (Institut National de Recherche en Informatique
1385 et en Automatique), France},
1386 type = {Technical Report},
1389 author_acronym = {WernerB},
1390 bibdate = {May 1, 1997},
1391 source = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/},
1392 source-date = {Mon 11 Sep 100},
1393 title_acronym = {coqpar}
1396 @unpublished{bw:1997,
1397 author = "Bruno Barras and Benjamin Werner",
1398 title = "{Coq in Coq}",
1401 ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz",
1404 @unpublished{berners-lee:1989,
1405 author = "Tim Berners-Lee",
1406 title = "{Information Management: A Proposal}",
1408 ps = "http://www.w3.org/History/1989/proposal.html",
1411 @techreport{natural,
1412 author = "Yann Coscoy and Gilles Kahn and Laurent Thery",
1413 title = "{Extracting Text from Proofs}",
1414 institution = {Inria (Institut National de Recherche en Informatique
1415 et en Automatique), France},
1416 type = {Technical Report},
1421 @inproceedings{Bru80,
1422 author = "de Bruijn, N. G.",
1423 title = "{A survey of the project AUTOMATH}",
1425 editor = "J. P. Seldin and J. R. Hindley",
1426 booktitle = "To H. B. Curry: Essays in Combinatory Logic,
1427 Lambda Calculus and Formalism",
1429 publisher = "Academic Press"
1432 @techreport{tutrect,
1433 author = "E Gim\'enez",
1434 title = "{A Tutorial on Recursive Types in Coq}",
1435 institution = {Inria (Institut National de Recherche en Informatique
1436 et en Automatique), France},
1437 type = {Technical Report},
1443 author = "John Harrison",
1444 title = "{The QED Manifesto}",
1446 booktitle = "Automated Deduction - CADE 12",
1447 series = "Lecture Notes in Artificial Intelligence",
1450 publisher = "Springer-Verlag"
1453 @inproceedings{harrison-mizar,
1454 author = "John Harrison",
1455 title = "{A Mizar Mode for HOL}",
1457 editor = "Joakim von Wright and Jim Grundy and John Harrison",
1458 booktitle = "Theorem Proving in Higher Order Logics:
1459 9th International Conference, TPHOLs'96",
1460 series = "Lecture Notes in Computer Science",
1462 address = "Turku, Finland",
1463 date = "26--30 August 1996",
1465 publisher = "Springer-Verlag"
1468 @inproceedings{proverb,
1469 author="H. Horacek",
1470 title="{Presenting Proofs in a Human Oriented Way}",
1471 booktitle="16th International Conference on Automated Deduction",
1476 author = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring",
1477 title = "{The Coq Proof Assistant. A Tutorial}",
1482 author="{Jutting van L. S. B.}",
1483 school = {{Eindhoven University of Technology}},
1484 title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}",
1485 type = {Ph D. thesis},
1486 note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}",
1490 @misc{abriefhistoryoftheinternet,
1491 author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.}
1492 and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.}
1493 and {Postel J.} and {Roberts L. G.} and {Wolff S.}",
1494 title="{A Brief Hystory of the Internet}",
1495 note="http://www.isoc.org/internet-history/brief.html"
1498 @inproceedings{MacKenzie:1995,
1499 author="{MacKenzie D.}",
1500 title="{The automation of proof: A historical and sociological exploration}",
1501 booktitle="IEEE: Annals of the History of Computing",
1506 author = "Christine Paulin-Mohring",
1508 school = {{Paris 7}},
1509 title = "{Extraction de programmes dans le Calcul des Constructions}",
1510 type = {Th\`ese d'universit\'e},
1512 url = {http://www.lri.fr/~paulin/these.ps.gz},
1516 author = "A. Ricci",
1517 school = {{Universit\`a degli studi di Bologna}},
1518 title = "{Studio e progettazione di un modello RDF per biblioteche matematiche
1520 type = {Tesi universitaria},
1524 @inproceedings{Rob65,
1525 author="{Robinson J. A.}",
1526 title = "{A machine-oriented logic based on the resolution principle}",
1528 booktitle = "Journal of the ACM",
1533 @inproceedings{sh:1995,
1534 author="{Saibi A.} and {Huet G.}",
1535 title="{Constructive Category Theory}",
1536 booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory",
1537 address="Goteborg (Sweden)",
1542 @inproceedings{ranta2,
1543 author="Thomas Hallgren and Aarne Ranta",
1544 title="An extensible proof text editor",
1545 BOOKTITLE = {LPAR'2000},
1546 SERIES = {LNCS/LNAI},
1551 @inproceedings{werner:1997,
1552 author="Benjamin Werner",
1553 title="{Constructive Category Theory}",
1554 booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software",