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, (to appear)",
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/}",
955 author = "Freek Wiedijk",
958 @misc{mowgli-deliverables,
959 title = "{MoWGLI} Project Deliverables",
960 howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html}",
961 key = "MoWGLI Deliverables"
965 title = "The {ALF} family of proof-assistants",
966 howpublished = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
967 url = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
972 title = "The {C}oq Proof Assistant Reference Manual",
973 author = "The Coq Development Team",
974 howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
979 title = "The {C}oq proof-assistant",
980 howpublished = "\\\url{http://coq.inria.fr}",
985 title = "The {PhoX} proof-assistant",
986 howpublished = "\\\url{http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html}",
991 title = "The {L}ego proof-assistant",
992 howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}",
993 url = "\url{http://www.dcs.ed.ac.uk/home/lego/}",
998 title = "The {A}lfa proof editor",
999 howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
1000 url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
1005 title = "The {PVS} Specification and Verification System",
1006 howpublished = "\\\url{http://pvs.csl.sri.com/}",
1011 title = "The {Isabelle} proof-assistant",
1012 howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}",
1017 author = "Constable, Robert L. and Stuart F. Allen and H. M. Bromley and
1018 W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and
1019 T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
1021 title = "Implementing Mathematics with the {N}uprl Development System",
1022 publisher = "Prentice-Hall",
1028 title = "The {NuPRL} proof-assistant",
1029 howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
1034 title = "The {HOL Light} proof-assistant",
1035 howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}",
1040 title = "The {MONET} project",
1041 howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}",
1046 title = "The {CALCULEMUS} project",
1047 howpublished = "\url{http://www.calculemus.net/}",
1048 url = "\url{http://www.calculemus.net/}",
1053 title = "The {M}izar proof-assistant",
1054 howpublished = "\\\url{http://mizar.uwb.edu.pl/}",
1059 howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium",
1060 author = "O. Caprotti and D. P. Carlisle and A. M. Cohen",
1061 title = "{\emph{The {O}pen{M}ath {S}tandard}}"
1065 title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
1066 editor="{Patrick Ion} and others",
1067 howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
1068 url = "\url{http://www.w3.org/TR/MathML2}",
1069 key = "Mathematical"
1073 title = "{E}xtensible {M}arkup {L}anguage ({XML}). {V}ersion 1.0.",
1074 editor="{Tim Bray} and others",
1075 howpublished = "W3C Recommendation 10 February 1998,
1076 \url{http://www.w3.org/TR/REC-xml}",
1077 url = "\url{http://www.w3.org/TR/REC-xml}",
1082 title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0",
1083 howpublished = "W3C Candidate Recommendation 10 May 2000,
1084 \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1085 url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1090 title = "Universal Resource Identifiers in {WWW}",
1091 howpublished = "RFC 1630, CERN",
1098 title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0",
1099 howpublished = "W3C Recommendation, 16 November 1999,
1100 \url{http://www.w3.org/TR/xpath}",
1101 url = "\url{http://www.w3.org/TR/xpath}",
1106 title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0",
1107 howpublished = "W3C Recommendation, 16 November 1999,
1108 \url{http://www.w3.org/TR/xslt}",
1109 url = "\url{http://www.w3.org/TR/xslt}",
1114 title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax
1116 howpublished = "W3C Recommendation 22 February 1999,
1117 \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1118 url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1123 title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)",
1124 howpublished = "\\\url{http://www.mathweb.org/omdoc/omdoc.ps}",
1129 title = "The {F}ormavie project",
1130 howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1131 url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1136 title = "The {HELM} project",
1137 howpublished = "\url{http://helm.cs.unibo.it}",
1138 url = "\url{http://helm.cs.unibo.it}",
1143 title = "The {HELM} On-Line Library",
1144 howpublished = "\url{http://helm.cs.unibo.it/library.html}",
1145 url = "\url{http://helm.cs.unibo.it/library.html}",
1146 key = "HELM Library"
1150 title = "The {M}ath{W}eb project",
1151 howpublished = "\url{http://www.mathweb.org}",
1152 url = "\url{http://www.mathweb.org}",
1157 title = "The {PC}oq project",
1158 howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1159 url = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1164 author = "Andrea Asperti and Luca Padovani and Claudio {Sacerdoti Coen}
1166 title = "Towards a library of formal mathematics",
1168 note = "Panel session of the 13th {I}nternation {C}onference on
1169 {T}heorem {P}roving in {H}igher {O}rder {L}ogics
1170 ({TPHOLS}'2000), Portland, Oregon, USA",
1173 @inproceedings{Ring,
1174 author = "Samuel Boutin",
1175 title = "Using Reflection to Build Efficient and Certified Decision
1177 editor = "Martin Abadi and Takahashi Ito editors",
1178 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1181 publisher = "Springer-Verlag",
1185 @inproceedings{werner-zfc,
1186 author = "Benjamin Werner",
1187 title = "Sets in Types, Types in Sets",
1188 editor = "Martin Abadi and Takahashi Ito editors",
1189 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1192 publisher = "Springer-Verlag",
1197 author = "Peter Aczel",
1198 title = "On Relating Type Theories and Set Theories",
1199 journal = "Lecture Notes in Computer Science",
1204 @inproceedings{remathematization,
1205 author = "Andrea Asperti and Luca Padovani
1206 and Claudio {Sacerdoti Coen} and Irene Schena",
1207 title = "{XML}, Stylesheets and the re-mathematization
1209 booktitle = "EXTREME",
1214 @phdthesis{YANNTHESIS,
1215 author = "Yann Coscoy",
1216 title = "Explication textuelle de preuves pour le {C}alcul des
1217 {C}onstructions {I}nductives",
1218 school = "Universit\'e de Nice-Sophia Antipolis",
1223 author = "Sylvain Lippi",
1224 title = "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)",
1225 school = "Universit\'e Aix-Marseille 2",
1230 author = "Benjamin Werner",
1231 title = "Une Th\'eorie des {C}onstructions {I}nductives",
1232 school = "Universit\'e Paris VII",
1237 @InCollection{Felleisen87,
1238 author = "M. Felleisen and D. Friedman",
1239 editor = "M. Wirsing",
1240 title = "Control operators, the {SECD}-machine, and the lambda calculus",
1241 booktitle = "Formal Description of Programming Concepts III",
1243 publisher = "Elsevier Science Publishers B.V.",
1244 address = "(North-Holland) Amsterdam",
1249 author = "Jan Zwanenburg",
1250 institution = "Eindhoven University of Technology",
1251 number = "Computing Science Report CS-98-11",
1252 title = "The Proof-assistant Yarrow",
1256 @TechReport{Ager2003a,
1257 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1258 institution = "BRICS",
1260 number = "BRICS RS-03-13",
1261 title = "A Functional Correspondence between Evaluators and Abstract Machines",
1265 @TechReport{Ager2003b,
1266 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1267 institution = "BRICS",
1269 number = "BRICS RS-03-14",
1270 title = "From Interpreter to Compiler and Virtual Machine: A Functional Derivation",
1274 @article{harperpollack,
1275 author = "Robert Harper and Robert Pollack",
1276 title = "Type checking with universes",
1277 journal = "Theoretical Computer Science",
1283 @article{activemath,
1284 author = "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich",
1285 title = "Knowledge Representation and Management in {ActiveMath}",
1286 journal = "Annals of Mathematics and Artificial Intelligence",
1294 author = "Andrea Asperti and Ferruccio Guidi and Luca Padovani and
1295 Claudio {Sacerdoti Coen} and Irene Schena",
1296 title = "Mathematical Knowledge Management in {HELM}",
1297 journal = "Annals of Mathematics and Artificial Intelligence",
1304 @unpublished{formal-topology,
1305 author = "Giovanni Sambin",
1306 title = "Some points in formal topology",
1307 note = "To appear in Theoretical Computer Science",
1311 @TechReport{JohnHarrison:complexity-of-floating-point-proofs,
1312 author = "John Harrison",
1313 title = "Real Numbers in Real Applications",
1314 note = "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002",
1315 institution = "NASA",
1316 number = "NASA/CP-2002-211736",
1320 @inproceedings{kohlhase-anghelache,
1321 author = "Michael Kohlhase and Romeo Anghelache",
1322 title = "Towards Collaborative Content Management And Version Control For
1323 Structured Mathematical Knowledge",
1324 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
1325 booktitle = "Proceedings of the Second International Conference on
1326 Mathematical Knowledge Management, MKM 2003",
1328 volume = "LNCS, 2594",
1329 publisher = "Springer-Verlag",
1333 %%% Unused entries from my Master dissertation bibliography
1336 title="{Standard Generalized Markup Language (SGML)}",
1337 note="ISO 8879:1986",
1342 author = "Andrea Asperti and Luca Padovani
1343 and Claudio {Sacerdoti Coen} and Irene Schena",
1344 title = "{Content Centric Logical Environments}",
1345 note = "Short Presentation at LICS 2000",
1346 ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz",
1350 author = "Andrea Asperti and Luca Padovani
1351 and Claudio {Sacerdoti Coen} and Irene Schena",
1352 title = "{Formal Mathematics in MathML}",
1353 note = "To be presented at MathML International Conference 2000",
1357 author = "Andrea Asperti and Luca Padovani
1358 and Claudio {Sacerdoti Coen} and Irene Schena",
1359 title = "{Towards a Library of Formal Mathematics}",
1360 note = "Accepted at TPHOLS 2000",
1361 ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz",
1364 @techreport{mowgli:D4a,
1365 author = "Hanane Naciri and Luca Padovani",
1366 title = "{MathML} Rendering/Browsing Engine",
1367 type = {MoWGLI Report},
1370 howpublished = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}"
1373 @techreport{hazewinkel,
1374 author = "Michiel Hazewinkel",
1375 title = "Dynamic stochastic models for indexes and thesauri,
1376 identification clouds, and information retrieval and
1378 type = "{MKM Net Report}",
1379 howpublished = "\url{http://monet.nag.co.uk/mkm//index.html}"
1382 @techreport{BarrasB:coqpar,
1383 author = "{Barras B.} and {Boutin S.} and {Cornes C.}
1384 and {Courant J.} and {Filliatre J. C.}
1385 and {Gim\'enez E.} and {Herbelin H.} and {Huet G.}
1386 and {Munoz C.} and {Murthy C.} and {Parent C.}
1387 and {Paulin-Mohring C.} and {Saibi A.}
1389 title = "{The Coq Proof Assistant Reference Manual : Version
1391 institution = {Inria (Institut National de Recherche en Informatique
1392 et en Automatique), France},
1393 type = {Technical Report},
1396 author_acronym = {WernerB},
1397 bibdate = {May 1, 1997},
1398 source = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/},
1399 source-date = {Mon 11 Sep 100},
1400 title_acronym = {coqpar}
1403 @unpublished{bw:1997,
1404 author = "Bruno Barras and Benjamin Werner",
1405 title = "{Coq in Coq}",
1408 ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz",
1411 @unpublished{berners-lee:1989,
1412 author = "Tim Berners-Lee",
1413 title = "{Information Management: A Proposal}",
1415 ps = "http://www.w3.org/History/1989/proposal.html",
1418 @techreport{natural,
1419 author = "Yann Coscoy and Gilles Kahn and Laurent Thery",
1420 title = "{Extracting Text from Proofs}",
1421 institution = {Inria (Institut National de Recherche en Informatique
1422 et en Automatique), France},
1423 type = {Technical Report},
1428 @inproceedings{Bru80,
1429 author = "de Bruijn, N. G.",
1430 title = "{A survey of the project AUTOMATH}",
1432 editor = "J. P. Seldin and J. R. Hindley",
1433 booktitle = "To H. B. Curry: Essays in Combinatory Logic,
1434 Lambda Calculus and Formalism",
1436 publisher = "Academic Press"
1439 @techreport{tutrect,
1440 author = "E Gim\'enez",
1441 title = "{A Tutorial on Recursive Types in Coq}",
1442 institution = {Inria (Institut National de Recherche en Informatique
1443 et en Automatique), France},
1444 type = {Technical Report},
1450 author = "John Harrison",
1451 title = "{The QED Manifesto}",
1453 booktitle = "Automated Deduction - CADE 12",
1454 series = "Lecture Notes in Artificial Intelligence",
1457 publisher = "Springer-Verlag"
1460 @inproceedings{harrison-mizar,
1461 author = "John Harrison",
1462 title = "{A Mizar Mode for HOL}",
1464 editor = "Joakim von Wright and Jim Grundy and John Harrison",
1465 booktitle = "Theorem Proving in Higher Order Logics:
1466 9th International Conference, TPHOLs'96",
1467 series = "Lecture Notes in Computer Science",
1469 address = "Turku, Finland",
1470 date = "26--30 August 1996",
1472 publisher = "Springer-Verlag"
1475 @inproceedings{proverb,
1476 author="H. Horacek",
1477 title="{Presenting Proofs in a Human Oriented Way}",
1478 booktitle="16th International Conference on Automated Deduction",
1483 author = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring",
1484 title = "{The Coq Proof Assistant. A Tutorial}",
1489 author="{Jutting van L. S. B.}",
1490 school = {{Eindhoven University of Technology}},
1491 title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}",
1492 type = {Ph D. thesis},
1493 note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}",
1497 @misc{abriefhistoryoftheinternet,
1498 author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.}
1499 and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.}
1500 and {Postel J.} and {Roberts L. G.} and {Wolff S.}",
1501 title="{A Brief Hystory of the Internet}",
1502 note="http://www.isoc.org/internet-history/brief.html"
1505 @inproceedings{MacKenzie:1995,
1506 author="{MacKenzie D.}",
1507 title="{The automation of proof: A historical and sociological exploration}",
1508 booktitle="IEEE: Annals of the History of Computing",
1513 author = "Christine Paulin-Mohring",
1515 school = {{Paris 7}},
1516 title = "{Extraction de programmes dans le Calcul des Constructions}",
1517 type = {Th\`ese d'universit\'e},
1519 url = {http://www.lri.fr/~paulin/these.ps.gz},
1523 author = "A. Ricci",
1524 school = {{Universit\`a degli studi di Bologna}},
1525 title = "{Studio e progettazione di un modello RDF per biblioteche matematiche
1527 type = {Tesi universitaria},
1531 @inproceedings{Rob65,
1532 author="{Robinson J. A.}",
1533 title = "{A machine-oriented logic based on the resolution principle}",
1535 booktitle = "Journal of the ACM",
1540 @inproceedings{sh:1995,
1541 author="{Saibi A.} and {Huet G.}",
1542 title="{Constructive Category Theory}",
1543 booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory",
1544 address="Goteborg (Sweden)",
1549 @inproceedings{ranta2,
1550 author="Thomas Hallgren and Aarne Ranta",
1551 title="An extensible proof text editor",
1552 BOOKTITLE = {LPAR'2000},
1553 SERIES = {LNCS/LNAI},
1558 @inproceedings{werner:1997,
1559 author="Benjamin Werner",
1560 title="{Constructive Category Theory}",
1561 booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software",