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/}",
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/}",
995 url = "\url{http://www.dcs.ed.ac.uk/home/lego/}",
1000 title = "The {A}lfa proof editor",
1001 howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
1002 url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
1007 title = "The {PVS} Specification and Verification System",
1008 howpublished = "\\\url{http://pvs.csl.sri.com/}",
1013 title = "The {Isabelle} proof-assistant",
1014 howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}",
1019 author = "Constable, Robert L. and Stuart F. Allen and H. M. Bromley and
1020 W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and
1021 T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
1023 title = "Implementing Mathematics with the {N}uprl Development System",
1024 publisher = "Prentice-Hall",
1030 title = "The {NuPRL} proof-assistant",
1031 howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
1036 title = "The {HOL Light} proof-assistant",
1037 howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}",
1042 title = "The {MONET} project",
1043 howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}",
1048 title = "The {CALCULEMUS} project",
1049 howpublished = "\url{http://www.calculemus.net/}",
1050 url = "\url{http://www.calculemus.net/}",
1055 title = "The {M}izar proof-assistant",
1056 howpublished = "\\\url{http://mizar.uwb.edu.pl/}",
1061 howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium",
1062 author = "O. Caprotti and D. P. Carlisle and A. M. Cohen",
1063 title = "{\emph{The {O}pen{M}ath {S}tandard}}"
1067 title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
1068 editor="{Patrick Ion} and others",
1069 howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
1071 url = "\url{http://www.w3.org/TR/MathML2}",
1072 key = "Mathematical"
1076 title = "{E}xtensible {M}arkup {L}anguage ({XML}). {V}ersion 1.0.",
1077 editor="{Tim Bray} and others",
1078 howpublished = "W3C Recommendation 10 February 1998,
1079 \url{http://www.w3.org/TR/REC-xml}",
1080 url = "\url{http://www.w3.org/TR/REC-xml}",
1085 title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0",
1086 howpublished = "W3C Candidate Recommendation 10 May 2000,
1087 \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1088 url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1093 title = "Universal Resource Identifiers in {WWW}",
1094 howpublished = "RFC 1630, CERN",
1101 title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0",
1102 howpublished = "W3C Recommendation, 16 November 1999,
1103 \url{http://www.w3.org/TR/xpath}",
1104 url = "\url{http://www.w3.org/TR/xpath}",
1109 title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0",
1110 howpublished = "W3C Recommendation, 16 November 1999,
1111 \url{http://www.w3.org/TR/xslt}",
1112 url = "\url{http://www.w3.org/TR/xslt}",
1117 title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax
1119 howpublished = "W3C Recommendation 22 February 1999,
1120 \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1121 url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1126 title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)",
1127 howpublished = "\\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}",
1133 title = "The {F}ormavie project",
1134 howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1135 url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1140 title = "The {HELM} project",
1141 howpublished = "\url{http://helm.cs.unibo.it}",
1142 url = "\url{http://helm.cs.unibo.it}",
1147 title = "The {HELM} On-Line Library",
1148 howpublished = "\url{http://helm.cs.unibo.it/library.html}",
1149 url = "\url{http://helm.cs.unibo.it/library.html}",
1150 key = "HELM Library"
1154 title = "The {M}ath{W}eb project",
1155 howpublished = "\url{http://www.mathweb.org}",
1156 url = "\url{http://www.mathweb.org}",
1161 title = "The {PC}oq project",
1162 howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1163 url = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1168 author = "Andrea Asperti and Luca Padovani and Claudio {Sacerdoti Coen}
1170 title = "Towards a library of formal mathematics",
1172 note = "Panel session of the 13th {I}nternation {C}onference on
1173 {T}heorem {P}roving in {H}igher {O}rder {L}ogics
1174 ({TPHOLS}'2000), Portland, Oregon, USA",
1177 @inproceedings{Ring,
1178 author = "Samuel Boutin",
1179 title = "Using Reflection to Build Efficient and Certified Decision
1181 editor = "Martin Abadi and Takahashi Ito editors",
1182 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1185 publisher = "Springer-Verlag",
1189 @inproceedings{werner-zfc,
1190 author = "Benjamin Werner",
1191 title = "Sets in Types, Types in Sets",
1192 editor = "Martin Abadi and Takahashi Ito editors",
1193 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1196 publisher = "Springer-Verlag",
1201 author = "Peter Aczel",
1202 title = "On Relating Type Theories and Set Theories",
1203 journal = "Lecture Notes in Computer Science",
1208 @inproceedings{remathematization,
1209 author = "Andrea Asperti and Luca Padovani
1210 and Claudio {Sacerdoti Coen} and Irene Schena",
1211 title = "{XML}, Stylesheets and the re-mathematization
1213 booktitle = "EXTREME",
1218 @phdthesis{YANNTHESIS,
1219 author = "Yann Coscoy",
1220 title = "Explication textuelle de preuves pour le {C}alcul des
1221 {C}onstructions {I}nductives",
1222 school = "Universit\'e de Nice-Sophia Antipolis",
1227 author = "Sylvain Lippi",
1228 title = "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)",
1229 school = "Universit\'e Aix-Marseille 2",
1234 author = "Benjamin Werner",
1235 title = "Une Th\'eorie des {C}onstructions {I}nductives",
1236 school = "Universit\'e Paris VII",
1241 @InCollection{Felleisen87,
1242 author = "M. Felleisen and D. Friedman",
1243 editor = "M. Wirsing",
1244 title = "Control operators, the {SECD}-machine, and the lambda calculus",
1245 booktitle = "Formal Description of Programming Concepts III",
1247 publisher = "Elsevier Science Publishers B.V.",
1248 address = "(North-Holland) Amsterdam",
1253 author = "Jan Zwanenburg",
1254 institution = "Eindhoven University of Technology",
1255 number = "Computing Science Report CS-98-11",
1256 title = "The Proof-assistant Yarrow",
1260 @TechReport{Ager2003a,
1261 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1262 institution = "BRICS",
1264 number = "BRICS RS-03-13",
1265 title = "A Functional Correspondence between Evaluators and Abstract Machines",
1269 @TechReport{Ager2003b,
1270 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1271 institution = "BRICS",
1273 number = "BRICS RS-03-14",
1274 title = "From Interpreter to Compiler and Virtual Machine: A Functional Derivation",
1278 @article{harperpollack,
1279 author = "Robert Harper and Robert Pollack",
1280 title = "Type checking with universes",
1281 journal = "Theoretical Computer Science",
1287 @article{activemath,
1288 author = "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich",
1289 title = "Knowledge Representation and Management in {ActiveMath}",
1290 journal = "Annals of Mathematics and Artificial Intelligence",
1298 author = "Andrea Asperti and Ferruccio Guidi and Luca Padovani and
1299 Claudio {Sacerdoti Coen} and Irene Schena",
1300 title = "Mathematical Knowledge Management in {HELM}",
1301 journal = "Annals of Mathematics and Artificial Intelligence",
1308 @unpublished{formal-topology,
1309 author = "Giovanni Sambin",
1310 title = "Some points in formal topology",
1311 note = "To appear in Theoretical Computer Science",
1315 @TechReport{JohnHarrison:complexity-of-floating-point-proofs,
1316 author = "John Harrison",
1317 title = "Real Numbers in Real Applications",
1318 note = "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002",
1319 institution = "NASA",
1320 number = "NASA/CP-2002-211736",
1324 @inproceedings{kohlhase-anghelache,
1325 author = "Michael Kohlhase and Romeo Anghelache",
1326 title = "Towards Collaborative Content Management And Version Control For
1327 Structured Mathematical Knowledge",
1328 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
1329 booktitle = "Proceedings of the Second International Conference on
1330 Mathematical Knowledge Management, MKM 2003",
1332 volume = "LNCS, 2594",
1333 publisher = "Springer-Verlag",
1337 %%% Unused entries from my Master dissertation bibliography
1340 title="{Standard Generalized Markup Language (SGML)}",
1341 note="ISO 8879:1986",
1346 author = "Andrea Asperti and Luca Padovani
1347 and Claudio {Sacerdoti Coen} and Irene Schena",
1348 title = "{Content Centric Logical Environments}",
1349 note = "Short Presentation at LICS 2000",
1350 ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz",
1354 author = "Andrea Asperti and Luca Padovani
1355 and Claudio {Sacerdoti Coen} and Irene Schena",
1356 title = "{Formal Mathematics in MathML}",
1357 note = "To be presented at MathML International Conference 2000",
1361 author = "Andrea Asperti and Luca Padovani
1362 and Claudio {Sacerdoti Coen} and Irene Schena",
1363 title = "{Towards a Library of Formal Mathematics}",
1364 note = "Accepted at TPHOLS 2000",
1365 ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz",
1368 @techreport{mowgli:D4a,
1369 author = "Hanane Naciri and Luca Padovani",
1370 title = "{MathML} Rendering/Browsing Engine",
1371 type = {MoWGLI Report},
1374 howpublished = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}"
1377 @techreport{hazewinkel,
1378 author = "Michiel Hazewinkel",
1379 title = "Dynamic stochastic models for indexes and thesauri,
1380 identification clouds, and information retrieval and
1382 type = "{MKM Net Report}",
1383 howpublished = "\url{http://monet.nag.co.uk/mkm//index.html}"
1386 @techreport{BarrasB:coqpar,
1387 author = "{Barras B.} and {Boutin S.} and {Cornes C.}
1388 and {Courant J.} and {Filliatre J. C.}
1389 and {Gim\'enez E.} and {Herbelin H.} and {Huet G.}
1390 and {Munoz C.} and {Murthy C.} and {Parent C.}
1391 and {Paulin-Mohring C.} and {Saibi A.}
1393 title = "{The Coq Proof Assistant Reference Manual : Version
1395 institution = {Inria (Institut National de Recherche en Informatique
1396 et en Automatique), France},
1397 type = {Technical Report},
1400 author_acronym = {WernerB},
1401 bibdate = {May 1, 1997},
1402 source = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/},
1403 source-date = {Mon 11 Sep 100},
1404 title_acronym = {coqpar}
1407 @unpublished{bw:1997,
1408 author = "Bruno Barras and Benjamin Werner",
1409 title = "{Coq in Coq}",
1412 ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz",
1415 @unpublished{berners-lee:1989,
1416 author = "Tim Berners-Lee",
1417 title = "{Information Management: A Proposal}",
1419 ps = "http://www.w3.org/History/1989/proposal.html",
1422 @techreport{natural,
1423 author = "Yann Coscoy and Gilles Kahn and Laurent Thery",
1424 title = "{Extracting Text from Proofs}",
1425 institution = {Inria (Institut National de Recherche en Informatique
1426 et en Automatique), France},
1427 type = {Technical Report},
1432 @inproceedings{Bru80,
1433 author = "de Bruijn, N. G.",
1434 title = "{A survey of the project AUTOMATH}",
1436 editor = "J. P. Seldin and J. R. Hindley",
1437 booktitle = "To H. B. Curry: Essays in Combinatory Logic,
1438 Lambda Calculus and Formalism",
1440 publisher = "Academic Press"
1443 @techreport{tutrect,
1444 author = "E Gim\'enez",
1445 title = "{A Tutorial on Recursive Types in Coq}",
1446 institution = {Inria (Institut National de Recherche en Informatique
1447 et en Automatique), France},
1448 type = {Technical Report},
1454 author = "John Harrison",
1455 title = "{The QED Manifesto}",
1457 booktitle = "Automated Deduction - CADE 12",
1458 series = "Lecture Notes in Artificial Intelligence",
1461 publisher = "Springer-Verlag"
1464 @inproceedings{harrison-mizar,
1465 author = "John Harrison",
1466 title = "{A Mizar Mode for HOL}",
1468 editor = "Joakim von Wright and Jim Grundy and John Harrison",
1469 booktitle = "Theorem Proving in Higher Order Logics:
1470 9th International Conference, TPHOLs'96",
1471 series = "Lecture Notes in Computer Science",
1473 address = "Turku, Finland",
1474 date = "26--30 August 1996",
1476 publisher = "Springer-Verlag"
1479 @inproceedings{proverb,
1480 author="H. Horacek",
1481 title="{Presenting Proofs in a Human Oriented Way}",
1482 booktitle="16th International Conference on Automated Deduction",
1487 author = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring",
1488 title = "{The Coq Proof Assistant. A Tutorial}",
1493 author="{Jutting van L. S. B.}",
1494 school = {{Eindhoven University of Technology}},
1495 title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}",
1496 type = {Ph D. thesis},
1497 note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}",
1501 @misc{abriefhistoryoftheinternet,
1502 author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.}
1503 and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.}
1504 and {Postel J.} and {Roberts L. G.} and {Wolff S.}",
1505 title="{A Brief Hystory of the Internet}",
1506 note="http://www.isoc.org/internet-history/brief.html"
1509 @inproceedings{MacKenzie:1995,
1510 author="{MacKenzie D.}",
1511 title="{The automation of proof: A historical and sociological exploration}",
1512 booktitle="IEEE: Annals of the History of Computing",
1517 author = "Christine Paulin-Mohring",
1519 school = {{Paris 7}},
1520 title = "{Extraction de programmes dans le Calcul des Constructions}",
1521 type = {Th\`ese d'universit\'e},
1523 url = {http://www.lri.fr/~paulin/these.ps.gz},
1527 author = "A. Ricci",
1528 school = {{Universit\`a degli studi di Bologna}},
1529 title = "{Studio e progettazione di un modello RDF per biblioteche matematiche
1531 type = {Tesi universitaria},
1535 @inproceedings{Rob65,
1536 author="{Robinson J. A.}",
1537 title = "{A machine-oriented logic based on the resolution principle}",
1539 booktitle = "Journal of the ACM",
1544 @inproceedings{sh:1995,
1545 author="{Saibi A.} and {Huet G.}",
1546 title="{Constructive Category Theory}",
1547 booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory",
1548 address="Goteborg (Sweden)",
1553 @inproceedings{ranta2,
1554 author="Thomas Hallgren and Aarne Ranta",
1555 title="An extensible proof text editor",
1556 BOOKTITLE = {LPAR'2000},
1557 SERIES = {LNCS/LNAI},
1562 @inproceedings{werner:1997,
1563 author="Benjamin Werner",
1564 title="{Constructive Category Theory}",
1565 booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software",