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 = "Claudio {Sacerdoti Coen}",
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}
463 and Enrico Tassi and Stefano Zacchiroli",
464 title = "A content based mathematical search engine: Whelp",
465 booktitle = "Post-proceedings of the Types 2004 International Conference",
466 volume = "LNCS, 3839",
468 publisher = "Springer-Verlag",
472 @inproceedings{exportation-module,
473 author = "Claudio {Sacerdoti Coen}",
474 title = "From Proof-Assistans to Distributed Libraries of Mathematics: Tips
476 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
477 booktitle = "Proceedings of the Second International Conference on
478 Mathematical Knowledge Management, MKM 2003",
480 volume = "LNCS, 2594",
481 publisher = "Springer-Verlag",
486 author = "Andrea Asperti and Herman Geuvers and Iris Loeb
487 and Lionel Elie Mamane and Claudio {Sacerdoti Coen}",
488 title = "An Interactive Algebra Course with Formalised Proofs and Definitions",
489 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
490 booktitle = "Post-Proceedings of the Fourth International Conference on Mathematical Knowledge Management, MKM 2005",
492 volume = "LNCS, (to appear)",
493 publisher = "Springer-Verlag",
497 @inproceedings{davenport,
498 author = "James H. Davenport",
499 title = "{MKM} from Book to Computer: A Case Study",
500 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
501 booktitle = "Proceedings of the Second International Conference on
502 Mathematical Knowledge Management, MKM 2003",
504 volume = "LNCS, 2594",
505 publisher = "Springer-Verlag",
509 @inproceedings{fguidisacerdot,
510 author = "Ferruccio Guidi and Claudio {Sacerdoti Coen}",
511 title = "Querying Distributed Digital Libraries of Mathematics",
512 editor = "Therese Hardin and Renaud Rioboo",
513 booktitle = "Calculemus 2003",
515 publisher = "Aracne Editrice S.R.L.",
517 note = "ISBN 88-7999-545-6"
520 @inproceedings{hbugs,
521 author = "Claudio {Sacerdoti Coen} and Stefano Zacchiroli",
522 title = "Brokers and {W}eb-Services for Automatic Deduction: a Case Study",
523 editor = "Therese Hardin and Renaud Rioboo",
524 booktitle = "Calculemus 2003",
526 publisher = "Aracne Editrice S.R.L.",
528 note = "ISBN 88-7999-545-6"
531 @inproceedings{calculemus-presentation,
532 author = "Christoph Benzm{\"u}ller",
533 title = "The {CALCULEMUS} Research Training Network -- A short Overview",
534 editor = "Therese Hardin and Renaud Rioboo",
535 booktitle = "Calculemus 2003",
537 publisher = "Aracne Editrice S.R.L.",
539 note = "ISBN 88-7999-545-6"
542 @inproceedings{linda,
543 author = "Claudio {Sacerdoti Coen}",
544 title = "A Constructive Proof of the Soundness of the
545 Encoding of Random Access Machines in a Linda Calculus with Ordered
547 booktitle = "Theoretical Computer Science: 8th Italian Conference, ICTCS 2003",
549 volume = "LNCS, 2841",
550 publisher = "Springer-Verlag",
554 @article{asperti-categorical-understanding,
555 author = "Andrea Asperti",
556 title = "A categorical understanding of environment machines",
557 journal = "Journal of Functional Programming",
565 @article{namelessdummies,
566 author = "{N. G. de Bruijn}",
567 title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem",
568 journal = "Indagationes Mathematicae",
575 author = "Yves Bertot",
576 title = "The CtCoq System: Design and Architecture",
577 journal = "Formal Aspects of Computing",
584 author = "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
585 title = "Real Theorem Provers Deserve Real User-Interfaces",
588 institution = "INRIA",
589 number = "{Inria Research Report 1684}"
593 author = "Yves Bertot and Laurent Th\'ery",
594 title = "A Generic Approach to Building User Interfaces for Theorem Provers",
595 journal = "Journal of Symbolic Computation",
602 author = "Michael Kohlhase and Andreas Franke",
603 title = "{MBase}: Representing Knowledge and Context for the Integration of Mathematical Software Systems",
604 journal = "Journal of Symbolic Computation",
609 url = "\url{http://citeseer.nj.nec.com/kohlhase00mbase.html}"
612 @inproceedings{mizarql,
613 author = "Grzegorz Bancerek and Piotr Rudnicki",
614 title = "Information Retrieval in {MML}",
615 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
616 booktitle = "Proceedings of the Second International Conference on
617 Mathematical Knowledge Management, MKM 2003",
619 volume = "LNCS, 2594",
620 publisher = "Springer-Verlag",
624 @article{codedcontexttrees,
625 author = "Harald Ganzinger and Robert Nieuwehuis and Pilar Nivela",
626 title = "Fast Term Indexing with Coded Context Trees. Journal of Automated Reasoning",
627 journal = "Journal of Automated Reasoning",
632 author = "Aarne Ranta",
633 title = "Grammatical Framework: A Type-Theoretical Grammar Formalism",
634 journal = "Journal of Functional Programming",
636 note = "Manuscript made available in September 2002"
640 AUTHOR = "Di Cosmo, Roberto",
641 TITLE = {Isomorphisms of types: from $\lambda$-calculus to information retrieval and language design},
642 SERIES = {Progress in Theoretical Computer Science},
643 PUBLISHER = {Birkhauser},
645 NOTE = {ISBN-0-8176-3763-X}
649 EDITOR = "R.P. Nederpelt and J.H. Geuvers and R.C. de Vrijer",
650 TITLE = {Selected Papers on Automath},
651 SERIES = {Studies in Logic and the Foundations of Mathematics},
652 PUBLISHER = {Elsevier Science},
655 NOTE = {ISBN-0444898220}
659 author = "Jean-Louis Krivine",
660 title = "Un interpr\`ete du $\lambda$-calcul",
661 howpublished = "Brouillon. Available on-line at \url{http://www.logique.jussieu.fr/~krivine}",
666 title = "Progress Report: Building Interactive Digital Libraries of Formal
667 Algorithmic Knowledge",
668 howpublished = "Cornell University, \url{http://www.cs.uwyo.edu/~nuprl/documents/cornell_slides.pdf}",
674 @misc{metadata4education,
675 title = "{L}earning {O}bject {M}etadata Standard",
676 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+",
681 @misc{openmath-cd-with-plus,
682 title = "Arith1 {OpenMath} {C}ontent {D}ictionary",
683 howpublished = "The OpenMath Society, \url{http://www.openmath.org/cocoon/openmath/cd/arith1.ocd}",
685 key = "Arith1 OpenMath Content Dictionary"
690 title = "Dewey Decimal Classification",
691 howpublished = "\url{http://www.oclc.org/dewey}",
692 url = "\url{http://www.oclc.org/dewey}",
697 title = "Library of Congress Classification Scheme",
698 howpublished = "\url{http://www.loc.gov}",
699 url = "\url{http://www.loc.gov}",
704 title = "Mathematical {S}ubject {C}lassification, {A}merican {M}athematical {S}ociety",
705 howpublished = "\url{http://www.ams.org/msc}",
706 url = "\url{http://www.ams.org/msc}",
710 @InCollection{borges,
711 author = "Jorge Luis Borges",
712 title = "The Library of {B}abel",
713 publisher = "Grove Press",
714 booktitle = "Ficciones",
718 @inproceedings{magaud,
719 author = "Nicolas Magaud",
720 title = "{C}hanging {D}ata {R}epresentation within the {C}oq {S}ystem",
721 booktitle = {TPHOLs'2003},
722 publisher = {Springer-Verlag},
723 volume = {LNCS, 2758},
727 @inproceedings{geuvers-jojgov,
728 author = "Herman Geuvers and Gueorgui I. Jojgov",
729 title = "Open Proofs and Open Terms: A Basis for Interactive Logic",
730 editor = "J. Bradfield",
731 booktitle = "Computer Science Logic: 16th International Workshop, CLS 2002",
733 volume = "LNCS, 2471",
734 publisher = "Springer-Verlag",
739 @inproceedings{mkm-structure,
740 author = "Koji Nakagawa and Akihiro Nomura and Masakazu Suzuki",
741 title = "Extraction of Logical Structure from articles in Mathematics",
742 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
743 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
744 volume = "LNCS, 3119",
746 publisher = "Springer-Verlag",
750 @inproceedings{mkm-metadata2,
751 author = "Andrea Asperti and Matteo Selmi",
752 title = "Efficient Retrieval of Mathematical Statements",
753 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
754 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
755 volume = "LNCS, 3119",
757 publisher = "Springer-Verlag",
761 @inproceedings{adams,
762 author = "A. A. Adams",
763 title = "Digitisation, Representation and Formalisation: Digital
764 Libraries of Mathematics.",
765 editor = "A. Asperti, B. Buchberger, J.H. Davenport",
766 booktitle = "Proceedings of Mathematical Knowledge Management 2003",
767 volume = "LNCS, 2594",
769 publisher = "Springer-Verlag",
774 author = "Serge Autexier and Dieter Hutter and Heiko Mantel and Axel Schairer",
775 title = "Towards an Evolutionary Formal Software-Development Using {CASL}",
776 booktitle = "WADT99 Selected Papers Volume",
777 volume = "LNCS, 1827",
778 publisher = "Springer-Verlag",
782 @inproceedings{how-to-extract,
783 author = "Lu\'is Cruz Filipe and Bas Spitters",
784 title = "Program Extraction from large proof developments",
785 booktitle = "Proceedings of TPHOLS 2003",
786 editor = "D. Basin and B. Wolff",
787 volume = "LNCS, 2758",
788 publisher = "Springer-Verlag",
792 @inproceedings{click-and-prove,
793 author = "Jean-Raymond Abrial and Dominique Cansell",
794 title = "Click'n {P}rove: Interactive Proofs Within Set Theory",
795 booktitle = "Proceedings of TPHOLS 2003",
796 editor = "D. Basin and B. Wolff",
797 volume = "LNCS, 2758",
798 publisher = "Springer-Verlag",
802 @inproceedings{delahaye,
803 author = "David Delahaye and Roberto di Cosmo",
804 title = "Information Retrieval in a {C}oq Proof Library using
806 booktitle = "Proceedings of TYPES 99",
808 publisher = "Springer-Verlag",
813 author = "G. I. Jojgov",
814 title = "Systems for open terms: An Overview",
815 institution = "Technische Universiteit Eindhoven",
816 number = "CSR 01-03",
820 @TechReport{garrigue:implicit-arguments,
821 author = "Jun P. Furuse and Jacques Garrigue",
822 title = " A label-selective lambda-calculus with optional arguments and its compilation method",
823 institution = "Research Institute for Mathematical Sciences, Kyoto University",
824 number = "RIMS Preprint 1041",
830 author = "Alexandre Miquel",
831 title = "Le {C}alcul des {C}onstructions {I}mplicite: syntaxe et s\'emantique",
832 school = "Universit\'e Paris 7",
836 @phdthesis{chrzaszcz,
837 author = "Jacek Chrz{\c{a}}szcs",
838 title = "Modules in Type Theory with Generative Definitions",
839 school = "Uniwersytet Warszawski and Universit\'e de Paris Sud",
844 author = "Olivier Pons",
845 title = "Conception et r\'ealisation d'outils d'aide au d\'eveloppement de grosse th\'eories dans les syst\`emes de preuves interactifs",
846 school = "Conservatoire National des Arts et M\'etiers",
851 author = "Fr\'ed\'eric Blanqui",
852 title = "Type Theory and Rewriting",
853 school = "Universit\'e Paris XI",
857 @phdthesis{magnusson,
858 author = "Lena Magnusson",
859 title = "The Implementation of {ALF} -- a Proof Editor based
860 on Martin-L{\"o}f Monomorphic Type Theory with Explicit
862 school = "Chalmers University of Technology / G{\"o}teborg University",
867 author = "Conor McBride",
868 title = "Dependently Typed Functional Programs and their Proofs",
869 school = "University of Edinburgh",
874 author = "Irene Schena",
875 title = "Towards a Semantic Web for Formal Mathematics",
876 school = "University of Bologna",
881 author = "Ferruccio Guidi",
882 title = "Searching and Retrieving in Content-Based Repositories
883 of Formal Mathematical Knowledge",
884 school = "University of Bologna",
887 note = "Technical Report UBLCS 2003-06"
891 author = "Luca Padovani",
892 title = "MathML Formatting",
893 school = "University of Bologna",
896 note = "Technical Report UBLCS 2003-03"
899 @mastersthesis{csc-master,
900 author = "Claudio {Sacerdoti Coen}",
901 title = "Progettazione e realizzazione con tecnologia {XML} di basi distribuite di conoscenza matematica formalizzata",
902 school = "University of Bologna",
906 @mastersthesis{zack-master,
907 author = "Stefano Zacchiroli",
908 title = "Web {s}ervices per il supporto alla dimostrazione interattiva",
909 school = "University of Bologna",
913 @mastersthesis{dilena,
914 author = "Pietro Dilena",
915 title = "Generazione automatica di stylesheet per notazione matematica",
916 school = "University of Bologna",
921 author = "C\'esar Munoz",
922 title = "A Calculus of Substitutions for Incomplete-Proof
923 Representation in Type Theory",
930 author = "Martin Strecker",
931 title = "Construction and Deduction in Type Theories",
932 school = "Universit{\"a}t Ulm",
936 @misc{content-centric,
937 author = "Andrea Asperti and Luca padovani
938 and Claudio {Sacerdoti Coen} and irene Schena",
939 title = "Content-centric Logical Envirnoments",
940 howpublished = "Short Presentation at the Fifteenth IEEE Symposium on Logic in Computer Science",
943 key = "content centric"
946 @misc{mowgli-proposal,
947 title = "The {MoWGLI Proposal}, {HTML} Version",
948 howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/project.html}",
949 key = "MoWGLI Proposal"
952 @misc{debrujinfactor,
953 title = "The ``de Bruijn factor''",
954 howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}",
956 author = "Freek Wiedijk",
959 @misc{mowgli-deliverables,
960 title = "{MoWGLI} Project Deliverables",
961 howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html}",
962 key = "MoWGLI Deliverables"
966 title = "The {ALF} family of proof-assistants",
967 howpublished = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
968 url = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
973 title = "The {C}oq Proof Assistant Reference Manual",
974 author = "{The Coq Development Team}",
975 howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
981 title = "The {C}oq proof-assistant",
982 howpublished = "\\\url{http://coq.inria.fr}",
987 title = "The {PhoX} proof-assistant",
988 howpublished = "\\\url{http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html}",
993 title = "The {L}ego proof-assistant",
994 howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}",
999 title = "The {A}lfa proof editor",
1000 howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
1001 url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
1006 title = "The {PVS} Specification and Verification System",
1007 howpublished = "\\\url{http://pvs.csl.sri.com/}",
1012 title = "The {Isabelle} proof-assistant",
1013 howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}",
1018 author = "Constable, Robert L. and Stuart F. Allen and H. M. Bromley and
1019 W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and
1020 T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
1022 title = "Implementing Mathematics with the {N}uprl Development System",
1023 publisher = "Prentice-Hall",
1029 title = "The {NuPRL} proof-assistant",
1030 howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
1035 title = "The {HOL Light} proof-assistant",
1036 howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}",
1041 title = "The {MONET} project",
1042 howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}",
1047 title = "The {CALCULEMUS} project",
1048 howpublished = "\url{http://www.calculemus.net/}",
1049 url = "\url{http://www.calculemus.net/}",
1054 title = "The {M}izar proof-assistant",
1055 howpublished = "\\\url{http://mizar.uwb.edu.pl/}",
1060 howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium",
1061 author = "O. Caprotti and D. P. Carlisle and A. M. Cohen",
1062 title = "{\emph{The {O}pen{M}ath {S}tandard}}"
1066 title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
1067 editor="{Patrick Ion} and others",
1068 howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
1070 url = "\url{http://www.w3.org/TR/MathML2}",
1075 title = "{E}xtensible {M}arkup {L}anguage ({XML}). {V}ersion 1.0.",
1076 editor="{Tim Bray} and others",
1077 howpublished = "W3C Recommendation 10 February 1998,
1078 \url{http://www.w3.org/TR/REC-xml}",
1079 url = "\url{http://www.w3.org/TR/REC-xml}",
1084 title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0",
1085 howpublished = "W3C Candidate Recommendation 10 May 2000,
1086 \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1087 url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1092 title = "Universal Resource Identifiers in {WWW}",
1093 howpublished = "RFC 1630, CERN",
1100 title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0",
1101 howpublished = "W3C Recommendation, 16 November 1999,
1102 \url{http://www.w3.org/TR/xpath}",
1103 url = "\url{http://www.w3.org/TR/xpath}",
1108 title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0",
1109 howpublished = "W3C Recommendation, 16 November 1999,
1110 \url{http://www.w3.org/TR/xslt}",
1111 url = "\url{http://www.w3.org/TR/xslt}",
1116 title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax
1118 howpublished = "W3C Recommendation 22 February 1999,
1119 \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1120 url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1125 title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)",
1126 howpublished = "\\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}",
1132 title = "The {F}ormavie project",
1133 howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1134 url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1139 title = "The {HELM} project",
1140 howpublished = "\url{http://helm.cs.unibo.it}",
1141 url = "\url{http://helm.cs.unibo.it}",
1146 title = "The {HELM} On-Line Library",
1147 howpublished = "\url{http://helm.cs.unibo.it/library.html}",
1148 url = "\url{http://helm.cs.unibo.it/library.html}",
1149 key = "HELM Library"
1153 title = "The {M}ath{W}eb project",
1154 howpublished = "\url{http://www.mathweb.org}",
1155 url = "\url{http://www.mathweb.org}",
1160 title = "The {PC}oq project",
1161 howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1162 url = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1167 author = "Andrea Asperti and Luca Padovani and Claudio {Sacerdoti Coen}
1169 title = "Towards a library of formal mathematics",
1171 note = "Panel session of the 13th {I}nternation {C}onference on
1172 {T}heorem {P}roving in {H}igher {O}rder {L}ogics
1173 ({TPHOLS}'2000), Portland, Oregon, USA",
1176 @inproceedings{Ring,
1177 author = "Samuel Boutin",
1178 title = "Using Reflection to Build Efficient and Certified Decision
1180 editor = "Martin Abadi and Takahashi Ito editors",
1181 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1184 publisher = "Springer-Verlag",
1188 @inproceedings{werner-zfc,
1189 author = "Benjamin Werner",
1190 title = "Sets in Types, Types in Sets",
1191 editor = "Martin Abadi and Takahashi Ito editors",
1192 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1195 publisher = "Springer-Verlag",
1200 author = "Peter Aczel",
1201 title = "On Relating Type Theories and Set Theories",
1202 journal = "Lecture Notes in Computer Science",
1207 @inproceedings{remathematization,
1208 author = "Andrea Asperti and Luca Padovani
1209 and Claudio {Sacerdoti Coen} and Irene Schena",
1210 title = "{XML}, Stylesheets and the re-mathematization
1212 booktitle = "EXTREME",
1217 @phdthesis{YANNTHESIS,
1218 author = "Yann Coscoy",
1219 title = "Explication textuelle de preuves pour le {C}alcul des
1220 {C}onstructions {I}nductives",
1221 school = "Universit\'e de Nice-Sophia Antipolis",
1226 author = "Sylvain Lippi",
1227 title = "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)",
1228 school = "Universit\'e Aix-Marseille 2",
1233 author = "Benjamin Werner",
1234 title = "Une Th\'eorie des {C}onstructions {I}nductives",
1235 school = "Universit\'e Paris VII",
1240 @InCollection{Felleisen87,
1241 author = "M. Felleisen and D. Friedman",
1242 editor = "M. Wirsing",
1243 title = "Control operators, the {SECD}-machine, and the lambda calculus",
1244 booktitle = "Formal Description of Programming Concepts III",
1246 publisher = "Elsevier Science Publishers B.V.",
1247 address = "(North-Holland) Amsterdam",
1252 author = "Jan Zwanenburg",
1253 institution = "Eindhoven University of Technology",
1254 number = "Computing Science Report CS-98-11",
1255 title = "The Proof-assistant Yarrow",
1259 @TechReport{Ager2003a,
1260 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1261 institution = "BRICS",
1263 number = "BRICS RS-03-13",
1264 title = "A Functional Correspondence between Evaluators and Abstract Machines",
1268 @TechReport{Ager2003b,
1269 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1270 institution = "BRICS",
1272 number = "BRICS RS-03-14",
1273 title = "From Interpreter to Compiler and Virtual Machine: A Functional Derivation",
1277 @article{harperpollack,
1278 author = "Robert Harper and Robert Pollack",
1279 title = "Type checking with universes",
1280 journal = "Theoretical Computer Science",
1286 @article{activemath,
1287 author = "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich",
1288 title = "Knowledge Representation and Management in {ActiveMath}",
1289 journal = "Annals of Mathematics and Artificial Intelligence",
1297 author = "Andrea Asperti and Ferruccio Guidi and Luca Padovani and
1298 Claudio {Sacerdoti Coen} and Irene Schena",
1299 title = "Mathematical Knowledge Management in {HELM}",
1300 journal = "Annals of Mathematics and Artificial Intelligence",
1307 @unpublished{formal-topology,
1308 author = "Giovanni Sambin",
1309 title = "Some points in formal topology",
1310 note = "To appear in Theoretical Computer Science",
1314 @TechReport{JohnHarrison:complexity-of-floating-point-proofs,
1315 author = "John Harrison",
1316 title = "Real Numbers in Real Applications",
1317 note = "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002",
1318 institution = "NASA",
1319 number = "NASA/CP-2002-211736",
1323 @inproceedings{kohlhase-anghelache,
1324 author = "Michael Kohlhase and Romeo Anghelache",
1325 title = "Towards Collaborative Content Management And Version Control For
1326 Structured Mathematical Knowledge",
1327 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
1328 booktitle = "Proceedings of the Second International Conference on
1329 Mathematical Knowledge Management, MKM 2003",
1331 volume = "LNCS, 2594",
1332 publisher = "Springer-Verlag",
1336 %%% Unused entries from my Master dissertation bibliography
1339 title="{Standard Generalized Markup Language (SGML)}",
1340 note="ISO 8879:1986",
1345 author = "Andrea Asperti and Luca Padovani
1346 and Claudio {Sacerdoti Coen} and Irene Schena",
1347 title = "{Content Centric Logical Environments}",
1348 note = "Short Presentation at LICS 2000",
1349 ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz",
1353 author = "Andrea Asperti and Luca Padovani
1354 and Claudio {Sacerdoti Coen} and Irene Schena",
1355 title = "{Formal Mathematics in MathML}",
1356 note = "To be presented at MathML International Conference 2000",
1360 author = "Andrea Asperti and Luca Padovani
1361 and Claudio {Sacerdoti Coen} and Irene Schena",
1362 title = "{Towards a Library of Formal Mathematics}",
1363 note = "Accepted at TPHOLS 2000",
1364 ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz",
1367 @techreport{mowgli:D4a,
1368 author = "Hanane Naciri and Luca Padovani",
1369 title = "{MathML} Rendering/Browsing Engine",
1370 type = {MoWGLI Report},
1373 howpublished = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}"
1376 @techreport{hazewinkel,
1377 author = "Michiel Hazewinkel",
1378 title = "Dynamic stochastic models for indexes and thesauri,
1379 identification clouds, and information retrieval and
1381 type = "{MKM Net Report}",
1382 howpublished = "\url{http://monet.nag.co.uk/mkm//index.html}"
1385 @techreport{BarrasB:coqpar,
1386 author = "{Barras B.} and {Boutin S.} and {Cornes C.}
1387 and {Courant J.} and {Filliatre J. C.}
1388 and {Gim\'enez E.} and {Herbelin H.} and {Huet G.}
1389 and {Munoz C.} and {Murthy C.} and {Parent C.}
1390 and {Paulin-Mohring C.} and {Saibi A.}
1392 title = "{The Coq Proof Assistant Reference Manual : Version
1394 institution = {Inria (Institut National de Recherche en Informatique
1395 et en Automatique), France},
1396 type = {Technical Report},
1399 author_acronym = {WernerB},
1400 bibdate = {May 1, 1997},
1401 source = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/},
1402 source-date = {Mon 11 Sep 100},
1403 title_acronym = {coqpar}
1406 @unpublished{bw:1997,
1407 author = "Bruno Barras and Benjamin Werner",
1408 title = "{Coq in Coq}",
1411 ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz",
1414 @unpublished{berners-lee:1989,
1415 author = "Tim Berners-Lee",
1416 title = "{Information Management: A Proposal}",
1418 ps = "http://www.w3.org/History/1989/proposal.html",
1421 @techreport{natural,
1422 author = "Yann Coscoy and Gilles Kahn and Laurent Thery",
1423 title = "{Extracting Text from Proofs}",
1424 institution = {Inria (Institut National de Recherche en Informatique
1425 et en Automatique), France},
1426 type = {Technical Report},
1431 @inproceedings{Bru80,
1432 author = "de Bruijn, N. G.",
1433 title = "{A survey of the project AUTOMATH}",
1435 editor = "J. P. Seldin and J. R. Hindley",
1436 booktitle = "To H. B. Curry: Essays in Combinatory Logic,
1437 Lambda Calculus and Formalism",
1439 publisher = "Academic Press"
1442 @techreport{tutrect,
1443 author = "E Gim\'enez",
1444 title = "{A Tutorial on Recursive Types in Coq}",
1445 institution = {Inria (Institut National de Recherche en Informatique
1446 et en Automatique), France},
1447 type = {Technical Report},
1453 author = "John Harrison",
1454 title = "{The QED Manifesto}",
1456 booktitle = "Automated Deduction - CADE 12",
1457 series = "Lecture Notes in Artificial Intelligence",
1460 publisher = "Springer-Verlag"
1463 @inproceedings{harrison-mizar,
1464 author = "John Harrison",
1465 title = "{A Mizar Mode for HOL}",
1467 editor = "Joakim von Wright and Jim Grundy and John Harrison",
1468 booktitle = "Theorem Proving in Higher Order Logics:
1469 9th International Conference, TPHOLs'96",
1470 series = "Lecture Notes in Computer Science",
1472 address = "Turku, Finland",
1473 date = "26--30 August 1996",
1475 publisher = "Springer-Verlag"
1478 @inproceedings{proverb,
1479 author="H. Horacek",
1480 title="{Presenting Proofs in a Human Oriented Way}",
1481 booktitle="16th International Conference on Automated Deduction",
1486 author = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring",
1487 title = "{The Coq Proof Assistant. A Tutorial}",
1492 author="{Jutting van L. S. B.}",
1493 school = {{Eindhoven University of Technology}},
1494 title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}",
1495 type = {Ph D. thesis},
1496 note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}",
1500 @misc{abriefhistoryoftheinternet,
1501 author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.}
1502 and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.}
1503 and {Postel J.} and {Roberts L. G.} and {Wolff S.}",
1504 title="{A Brief Hystory of the Internet}",
1505 note="http://www.isoc.org/internet-history/brief.html"
1508 @inproceedings{MacKenzie:1995,
1509 author="{MacKenzie D.}",
1510 title="{The automation of proof: A historical and sociological exploration}",
1511 booktitle="IEEE: Annals of the History of Computing",
1516 author = "Christine Paulin-Mohring",
1518 school = {{Paris 7}},
1519 title = "{Extraction de programmes dans le Calcul des Constructions}",
1520 type = {Th\`ese d'universit\'e},
1522 url = {http://www.lri.fr/~paulin/these.ps.gz},
1526 author = "A. Ricci",
1527 school = {{Universit\`a degli studi di Bologna}},
1528 title = "{Studio e progettazione di un modello RDF per biblioteche matematiche
1530 type = {Tesi universitaria},
1534 @inproceedings{Rob65,
1535 author="{Robinson J. A.}",
1536 title = "{A machine-oriented logic based on the resolution principle}",
1538 booktitle = "Journal of the ACM",
1543 @inproceedings{sh:1995,
1544 author="{Saibi A.} and {Huet G.}",
1545 title="{Constructive Category Theory}",
1546 booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory",
1547 address="Goteborg (Sweden)",
1552 @inproceedings{ranta2,
1553 author="Thomas Hallgren and Aarne Ranta",
1554 title="An extensible proof text editor",
1555 BOOKTITLE = {LPAR'2000},
1556 SERIES = {LNCS/LNAI},
1561 @inproceedings{werner:1997,
1562 author="Benjamin Werner",
1563 title="{Constructive Category Theory}",
1564 booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software",
1568 @inproceedings{barthe95implicit,
1569 author = "Gilles Barthe",
1570 title = "Implicit Coercions in Type Systems",
1571 booktitle = "{TYPES}",
1574 url = "citeseer.ist.psu.edu/barthe95implicit.html" }