3 author = "Robert Nieuwenhuis and Alberto Rubio",
4 title = "Paramodulation-based thorem proving",
5 booktitle = "Handbook of Automated Reasoning",
7 publisher = "Elsevier and MIT Press",
9 NOTE = {ISBN-0-262-18223-8}
12 @inproceedings{latexmathml,
13 author = {Luca Padovani},
14 title = {On the Roles of LATEX and MathML in Encoding and Processing Mathematical Expressions},
15 booktitle = {MKM '03: Proceedings of the Second International Conference on Mathematical Knowledge Management},
17 isbn = {3-540-00568-4},
19 publisher = {Springer-Verlag},
20 address = {London, UK},
23 @inproceedings{gmetadom,
24 author = "Luca Padovani and Claudio {Sacerdoti Coen} and Stefano Zacchiroli",
25 title = "A Generative Approach to the Implementation of Language Bindings for the Document Object Model",
26 booktitle = "Generative Programming and Component Engineering",
27 editor = "Gabor Karsai and Eelco Visser",
31 publisher = "Springer-Verlag",
36 author = "Freek Wiedijk",
37 title = "MMode, a Mizar Mode for the proof assistant Coq",
38 institution = "University of Nijmegen",
39 number = "NIII-R0333",
43 @article{ lamport-proof,
44 author = "Leslie Lamport",
45 title = "How to write a proof",
46 journal = "American Mathematical Monthly",
53 @inproceedings{thery-authoring,
54 author = "Laurent {Th\'ery}",
55 title = "Formal Proof Authoring: an Experiment",
56 booktitle = "User Interface Design for Theorem Provers",
57 editor = "David Aspinall and Christoph L{\"u}th",
61 @inproceedings{padovani-editex,
62 author = "Luca Padovani",
63 title = "Interactive Editing of MathML Markup Using TeX Syntax",
64 booktitle = "International Conference on TeX, XML, and Digital Typography",
69 publisher = "Springer-Verlag",
72 @inproceedings{uitp-knowledge-modelling,
73 author = "Stuart Aitken",
74 title = "Problem Solving in Interactive Proof: A Knowledge-Modelling Approach",
75 booktitle = "European Conference on Artificial Intelligence (ECAI)",
79 @inproceedings{proof-by-pointing,
80 author = "Yves Bertot and Gilles Kahn and Laurent Th\'ery",
81 title = "Proof by Pointing",
82 booktitle = "Symposium on Theoretical Aspects Computer Software (STACS)",
83 series = "Lecture Notes in Computer Science",
88 @inproceedings{thery-cyp,
89 author = "Laurent Th\`ery",
90 title = "Colouring proofs: a lightweight approach to adding formal structure to proofs",
91 booktitle = "User Interface Design for Theorem Provers",
92 editor = "David Aspinall and Christoph L{\"u}th",
96 @article{uitp-empirical,
97 author = "Stuart Aitken and Phil Gray and Tom Melham and Muffy Thomas",
98 title = "Interactive Theorem Proving: An Empirical Study of User Activity",
99 journal = "Journal of Symbolic Computation",
103 @inproceedings{uitp-phases,
104 author = "Stuart Aitken and Phil Gray and Tom Melham and Muffy Thomas",
105 title = "Phases, Modes and Information Flow in Theory Development",
106 booktitle = "User Interface Design for Theorem Provers",
107 editor = "Nicholas Merriam",
111 @inproceedings{searchingmath,
112 author = "Andrea Asperti and Stefano Zacchiroli",
113 title = "Searching mathematics on the Web: state of the art and future developments",
114 booktitle = "New Developments in Electronic Publishing of Mathematics",
115 editor = "Bernd Wegner",
116 publisher = {FIZ Karlsruhe},
121 author = "K. Appel and W. Haken",
122 title = "Every planar map is four colorable.",
123 journal = {Illinois Journal of Mathematics},
129 @misc{freekcomparison,
130 author = "Freek Wiedijk",
131 title = "The Sixteen Provers of the World",
132 howpublished = "University of Nijmegen,\\\url{http://www.cs.ru.nl/~freek/comparison/comparison.ps.gz}"
136 title = "Zentralblatt MATH",
137 howpublished = "\url{http://www.emis.de/ZMATH/}"
141 author = "Michael J. C. Gordon and Robin Milner and C.P. Wadsworth",
142 title = "{Edinburgh LCF}: a Mechanised Logic of Computation",
143 series = {Lecture Notes in Computer Science},
145 publisher = {{Sprin\-ger-Verlag}},
150 author = "Claudio {Sacerdoti Coen}",
151 title = "Mathematical Knowledge Management and Interactive Theorem
153 school = "University of Bologna",
155 note = "Technical Report UBLCS 2004-5"
159 author = "Markus Wenzel",
160 title = "Isar - A Generic Interpretative Approach to Readable Formal Proof Documents",
161 booktitle = "Theorem Proving in Higher Order Logics",
166 @inproceedings{centaur,
167 author = "P. Borras and D. Clement and Th. Despeyrouz and J. Incerpi and G. Kahn and B. Lang and V. Pascual",
168 title = "{CENTAUR}: The System",
169 booktitle = "Proceedings of the {ACM} {SIGSOFT}/{SIGPLAN} Software Engineering Symposium on Practical Software Development Environments ({PSDE})",
170 journal = "SIGPLAN Notices",
173 publisher = "ACM Press",
174 address = "New York, NY",
177 url = "citeseer.nj.nec.com/borras88centaur.html"
180 @inproceedings{Leroy-manifest-types,
181 AUTHOR = "Xavier Leroy",
182 TITLE = "Manifest types, modules, and separate compilation",
183 BOOKTITLE = {21st symposium Principles of Programming Languages},
185 PUBLISHER = {ACM Press},
187 URL = {http://pauillac.inria.fr/~xleroy/publi/manifest-types-popl.ps.gz}
190 @inproceedings{overkilling,
191 author = "Claudio {Sacerdoti Coen}",
192 title = "Tactics in Modern Proof-Assistants: the Bad Habit of
194 booktitle = "Supplementary Proceedings of the 14th International
195 Conference TPHOLS 2001",
200 @inproceedings{omegaants1,
201 author = "Christoph Benzm{\"u}ller and Volker Sorge",
202 title = {{OANTS} -- An open approach at combining Interactive and Automated
204 booktitle = {Symbolic Computation and Automated Reasoning},
205 editor = {Manfred Kerber and Michael Kohlhase},
208 publisher = {A.K.Peters},
209 url = {www.ags.uni-sb.de/~chris/papers/C8.pdf}
213 author = "R. Fateman and T. Tokuyasu and B. Berman and N. Mitchell",
214 title = {Optical Character Recognition and Parsing of Typeset Mathematics},
215 journal = {Journal of Visual Communication And Image Representation},
221 url = {www.ags.uni-sb.de/~chris/papers/J4.pdf}
224 @article{newauthomath,
225 author = "Freek Wiedijk",
226 title = "A new implementation of {A}utomath",
227 journal = {Journal of Automated Reasoning},
234 author = "Paolo Casarini and Luca Padovani",
235 title = "The {G}nome {DOM} {E}ngine",
236 journal = "Markup Languages: Theory \& Practice",
241 publisher = "MIT Press",
246 author = "Christoph Benzm{\"u}ller and Mateja Jamnik and Manfred Kerber and
248 title = {Agent based Mathematical Reasoning},
249 journal = {Electronic Notes in Theoretical Computer Science, Elsevier},
254 url = {www.ags.uni-sb.de/~chris/papers/J4.pdf}
257 @inproceedings{Necula,
258 author = "George C. Necula and Peter Lee",
259 title = "Safe Kernel Extensions Without Run-Time Checking",
260 booktitle = "2nd Symposium on Operating Systems Design and Implementation ({OSDI} '96), October 28--31, 1996. Seattle, {WA}",
261 publisher = "USENIX",
262 address = "Berkeley, CA, USA",
266 url = "citeseer.nj.nec.com/necula96safe.html"
269 @inproceedings{courant,
270 AUTHOR = "Judica{\"e}l Courant",
271 TITLE = {Explicit Universes for the {C}alculus of {C}onstructions},
272 BOOKTITLE = {Theorem Proving in Higher Order Logics:
273 15th International Conference, TPHOLs 2002},
274 EDITOR = {Victor A. {Carre\~{n}o} and C\'{e}sar A. {Mu\~{n}oz} and Sofi\`{e}ne Tahar},
275 SERIES = {Lecture Notes in Computer Science},
279 PUBLISHER = {{Sprin\-ger-Verlag}},
281 ADDRESS = {Hampton, VA, USA}
285 author = "George C. Necula and Peter Lee",
286 title="{Efficient Representation and Validation of Proofs}",
287 booktitle="Proceedings of the 13th Annual symposium on Logic in Computer Science,",
288 address="Indianapolis",
293 author = "Jean-Yves Girard and Yves Lafont and Paul Taylor",
294 title = "{Proofs and Types}",
295 publisher = {Cambridge University Press},
296 series = {Cambridge Tracts in Theoretical Computer Science},
301 author = "Yves Bertot and Pierre Castéran",
302 title = "{Interactive Theorem Proving and Program Development}",
303 publisher = {Springer Verlag},
304 series = {Texts in Theoretical Computer Science},
306 NOTE = {ISBN-3-540-20854-2}
310 @inproceedings{proofgeneral,
311 author = "David Aspinall",
312 title = "{P}roof {G}eneral: A Generic Tool for Proof Development",
313 booktitle = "Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000",
318 publisher = "Springer-Verlag",
321 @inproceedings{Gim94,
322 author = "Eduardo Gim\'enez",
323 title = "{Codifying guarded definitions with recursive schemes}",
324 booktitle = "Types for Proofs and Programs: International Workshop, {TYPES '94}",
328 publisher = "Springer-Verlag",
329 note = "Extended version in LIP research report 95-07, ENS Lyon",
333 @incollection{BarendregtH:lawcwt,
334 author = "H. Barendregt",
335 title = "{Lambda Calculi with Types}",
336 booktitle = "{Handbook of Logic in Computer Science}",
337 editor = "{Abramsky, Samson and others}",
338 publisher = "{Oxford University Press}",
343 @inproceedings{coquand:1986,
344 author="Thierry Coquand",
345 title="{An Analysis of Girard's Paradox}",
346 booktitle="Symposium on Logic in Computer Science",
348 publisher="MA. IEEE press",
353 AUTHOR = "Christine Paulin-Mohring",
354 TITLE = {D\'efinitions Inductives en Th\'eorie des Types d'Ordre Sup\'rieur},
355 SCHOOL = {Universit\'e Claude Bernard Lyon I},
358 TYPE = {Habilitation \`a diriger les recherches},
359 URL = {http://www.lri.fr/~paulin/habilitation.ps.gz}
363 author = "Jacques Garrigue",
364 title = "{Label-Selective Lambda-Calculi and Transformation Calculi}",
365 school = "University of Tokyo, Department of Information Science",
370 @phdthesis{LuoZ:extcc,
371 author = "Zhaohui Luo",
372 title = "{An Extended Calculus of Constructions}",
373 school = "University of Edinburgh",
378 author = "Laurent Chicli",
379 title = "Sur la formalisation des math\'ematiques dans le
380 {C}alcul des {C}onstructions {I}nductives",
381 school = "Universit\'e de Nice~-~Sophia Antipolis",
385 @phdthesis{geuvers:1993,
386 author="Herman Geuvers",
387 title="{Logics and Type Systems}",
388 school="Catholic University Nijmegen",
390 type="{Ph.D.} dissertation"
393 @unpublished{PrimesInP,
394 author = "M. Agrawal and N. Kayal and N. Saxena",
395 title = "{PRIMES} in {P}",
396 note = "\url{http://www.cse.iitk.ac.in/users/manindra/primality.ps}",
401 @unpublished{danosKAM,
402 author = "Vincent Danos and Laurent Regnier",
403 title = "How abstract machines implement head linear reduction",
407 @inproceedings{Oostdijk,
408 author = "Olga Caprotti and Herman Geuvers and Martin Oostdijk",
409 title = "Certified and Portable Mathematical Documents from Formal Contexts",
410 editor = "Bruno Buchberger and Olga Caprotti",
411 booktitle = "On-Line Proceedings of the First International Conference on
412 Mathematical Knowledge Management, MKM 2001",
413 publisher = "The Electronic Library of Mathematics (EMIS)",
414 url = "\url{http://www.emis.de/ELibM.html}",
418 @inproceedings{formal-proof-sketches,
419 author = "Freek Wiedijk",
420 title = "Formal Proof Sketches",
421 editor = "Wan Fokkink and Jaco van de Pol",
422 booktitle = "7th Dutch Proof Tools Day, Program + Proceedings",
423 note = "CWI, Amsterdam",
427 @inproceedings{Barendregt,
428 author = "Henk Barendregt",
429 title = "Towards an Interactive Mathematical Proof Language",
430 editor = "Fairouz Kamareddine",
431 booktitle = "Thirty Five Years of Automath",
433 publisher = "Kluwer",
437 @inproceedings{werner:prof-irrelevance,
438 author = "Alexandre Miquel and Benjamin Werner",
439 title = "The Not So Simple Proof-Irrelevant Model of {CC}",
440 editor = "Herman Geuvers and Freek Wiedijk",
441 booktitle = "Types for Proofs and Programs: International Workshop, {TYPES 2002}",
443 volume = "LNCS, 2646",
444 publisher = "Springer-Verlag",
448 @inproceedings{csc-environment,
449 author = "Claudio {Sacerdoti Coen}",
450 title = "Mathematical Libraries as Proof Assistant Environments",
451 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
452 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
453 volume = "LNCS, 3119",
455 publisher = "Springer-Verlag",
459 @inproceedings{disambiguation,
460 author = "Claudio {Sacerdoti Coen} and Stefano Zacchiroli",
461 title = "Efficient Ambiguous Parsing of Mathematical Formulae",
462 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
463 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
464 volume = "LNCS, 3119",
466 publisher = "Springer-Verlag",
470 @inproceedings{pechino,
471 author = "Andrea Asperti and Bernd Wegner",
472 title = "An Approach to Machine-Understandable Representation of the Mathematical Information in Digital Documents",
473 editor = "Fengshai Bai and Bernd Wegner",
474 booktitle = "Electronic Information and Communication in Mathematics",
475 volume = "LNCS, 2730",
477 publisher = "Springer-Verlag",
481 @inproceedings{whelp,
482 author = "Andrea Asperti and Ferruccio Guidi and Claudio {Sacerdoti Coen}
483 and Enrico Tassi and Stefano Zacchiroli",
484 title = "A content based mathematical search engine: Whelp",
485 booktitle = "Post-proceedings of the Types 2004 International Conference",
486 volume = "LNCS, 3839",
488 publisher = "Springer-Verlag",
492 @inproceedings{exportation-module,
493 author = "Claudio {Sacerdoti Coen}",
494 title = "From Proof-Assistans to Distributed Libraries of Mathematics: Tips
496 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
497 booktitle = "Proceedings of the Second International Conference on
498 Mathematical Knowledge Management, MKM 2003",
500 volume = "LNCS, 2594",
501 publisher = "Springer-Verlag",
506 author = "Andrea Asperti and Herman Geuvers and Iris Loeb
507 and Lionel Elie Mamane and Claudio {Sacerdoti Coen}",
508 title = "An Interactive Algebra Course with Formalised Proofs and Definitions",
509 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
510 booktitle = "Post-Proceedings of the Fourth International Conference on Mathematical Knowledge Management, MKM 2005",
512 volume = "LNCS, (to appear)",
513 publisher = "Springer-Verlag",
517 @inproceedings{davenport,
518 author = "James H. Davenport",
519 title = "{MKM} from Book to Computer: A Case Study",
520 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
521 booktitle = "Proceedings of the Second International Conference on
522 Mathematical Knowledge Management, MKM 2003",
524 volume = "LNCS, 2594",
525 publisher = "Springer-Verlag",
529 @inproceedings{fguidisacerdot,
530 author = "Ferruccio Guidi and Claudio {Sacerdoti Coen}",
531 title = "Querying Distributed Digital Libraries of Mathematics",
532 editor = "Therese Hardin and Renaud Rioboo",
533 booktitle = "Calculemus 2003",
535 publisher = "Aracne Editrice S.R.L.",
537 note = "ISBN 88-7999-545-6"
540 @inproceedings{hbugs,
541 author = "Claudio {Sacerdoti Coen} and Stefano Zacchiroli",
542 title = "Brokers and {W}eb-Services for Automatic Deduction: a Case Study",
543 editor = "Therese Hardin and Renaud Rioboo",
544 booktitle = "Calculemus 2003",
546 publisher = "Aracne Editrice S.R.L.",
548 note = "ISBN 88-7999-545-6"
551 @inproceedings{calculemus-presentation,
552 author = "Christoph Benzm{\"u}ller",
553 title = "The {CALCULEMUS} Research Training Network -- A short Overview",
554 editor = "Therese Hardin and Renaud Rioboo",
555 booktitle = "Calculemus 2003",
557 publisher = "Aracne Editrice S.R.L.",
559 note = "ISBN 88-7999-545-6"
562 @inproceedings{linda,
563 author = "Claudio {Sacerdoti Coen}",
564 title = "A Constructive Proof of the Soundness of the
565 Encoding of Random Access Machines in a Linda Calculus with Ordered
567 booktitle = "Theoretical Computer Science: 8th Italian Conference, ICTCS 2003",
569 volume = "LNCS, 2841",
570 publisher = "Springer-Verlag",
574 @article{asperti-categorical-understanding,
575 author = "Andrea Asperti",
576 title = "A categorical understanding of environment machines",
577 journal = "Journal of Functional Programming",
585 @article{namelessdummies,
586 author = "{N. G. de Bruijn}",
587 title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem",
588 journal = "Indagationes Mathematicae",
595 author = "Yves Bertot",
596 title = "The CtCoq System: Design and Architecture",
597 journal = "Formal Aspects of Computing",
604 author = "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
605 title = "Real Theorem Provers Deserve Real User-Interfaces",
608 institution = "INRIA",
609 number = "{Inria Research Report 1684}"
613 author = "Yves Bertot and Laurent Th\'ery",
614 title = "A Generic Approach to Building User Interfaces for Theorem Provers",
615 journal = "Journal of Symbolic Computation",
622 author = "Michael Kohlhase and Andreas Franke",
623 title = "{MBase}: Representing Knowledge and Context for the Integration of Mathematical Software Systems",
624 journal = "Journal of Symbolic Computation",
629 url = "\url{http://citeseer.nj.nec.com/kohlhase00mbase.html}"
632 @inproceedings{mizarql,
633 author = "Grzegorz Bancerek and Piotr Rudnicki",
634 title = "Information Retrieval in {MML}",
635 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
636 booktitle = "Proceedings of the Second International Conference on
637 Mathematical Knowledge Management, MKM 2003",
639 volume = "LNCS, 2594",
640 publisher = "Springer-Verlag",
644 @article{codedcontexttrees,
645 author = "Harald Ganzinger and Robert Nieuwehuis and Pilar Nivela",
646 title = "Fast Term Indexing with Coded Context Trees. Journal of Automated Reasoning",
647 journal = "Journal of Automated Reasoning",
652 author = "Aarne Ranta",
653 title = "Grammatical Framework: A Type-Theoretical Grammar Formalism",
654 journal = "Journal of Functional Programming",
656 note = "Manuscript made available in September 2002"
660 AUTHOR = "Di Cosmo, Roberto",
661 TITLE = {Isomorphisms of types: from $\lambda$-calculus to information retrieval and language design},
662 SERIES = {Progress in Theoretical Computer Science},
663 PUBLISHER = {Birkhauser},
665 NOTE = {ISBN-0-8176-3763-X}
669 EDITOR = "R.P. Nederpelt and J.H. Geuvers and R.C. de Vrijer",
670 TITLE = {Selected Papers on Automath},
671 SERIES = {Studies in Logic and the Foundations of Mathematics},
672 PUBLISHER = {Elsevier Science},
675 NOTE = {ISBN-0444898220}
679 author = "Jean-Louis Krivine",
680 title = "Un interpr\`ete du $\lambda$-calcul",
681 howpublished = "Brouillon. Available on-line at \url{http://www.logique.jussieu.fr/~krivine}",
686 title = "Progress Report: Building Interactive Digital Libraries of Formal
687 Algorithmic Knowledge",
688 howpublished = "Cornell University, \url{http://www.cs.uwyo.edu/~nuprl/documents/cornell_slides.pdf}",
694 @misc{metadata4education,
695 title = "{L}earning {O}bject {M}etadata Standard",
696 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+",
701 @misc{openmath-cd-with-plus,
702 title = "Arith1 {OpenMath} {C}ontent {D}ictionary",
703 howpublished = "The OpenMath Society, \url{http://www.openmath.org/cocoon/openmath/cd/arith1.ocd}",
705 key = "Arith1 OpenMath Content Dictionary"
710 title = "Dewey Decimal Classification",
711 howpublished = "\url{http://www.oclc.org/dewey}",
712 url = "\url{http://www.oclc.org/dewey}",
717 title = "Library of Congress Classification Scheme",
718 howpublished = "\url{http://www.loc.gov}",
719 url = "\url{http://www.loc.gov}",
724 title = "Mathematical {S}ubject {C}lassification, {A}merican {M}athematical {S}ociety",
725 howpublished = "\url{http://www.ams.org/msc}",
726 url = "\url{http://www.ams.org/msc}",
730 @InCollection{borges,
731 author = "Jorge Luis Borges",
732 title = "The Library of {B}abel",
733 publisher = "Grove Press",
734 booktitle = "Ficciones",
738 @inproceedings{magaud,
739 author = "Nicolas Magaud",
740 title = "{C}hanging {D}ata {R}epresentation within the {C}oq {S}ystem",
741 booktitle = {TPHOLs'2003},
742 publisher = {Springer-Verlag},
743 volume = {LNCS, 2758},
747 @inproceedings{geuvers-jojgov,
748 author = "Herman Geuvers and Gueorgui I. Jojgov",
749 title = "Open Proofs and Open Terms: A Basis for Interactive Logic",
750 editor = "J. Bradfield",
751 booktitle = "Computer Science Logic: 16th International Workshop, CLS 2002",
753 volume = "LNCS, 2471",
754 publisher = "Springer-Verlag",
759 @inproceedings{mkm-structure,
760 author = "Koji Nakagawa and Akihiro Nomura and Masakazu Suzuki",
761 title = "Extraction of Logical Structure from articles in Mathematics",
762 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
763 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
764 volume = "LNCS, 3119",
766 publisher = "Springer-Verlag",
770 @inproceedings{mkm-metadata2,
771 author = "Andrea Asperti and Matteo Selmi",
772 title = "Efficient Retrieval of Mathematical Statements",
773 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
774 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
775 volume = "LNCS, 3119",
777 publisher = "Springer-Verlag",
781 @inproceedings{adams,
782 author = "A. A. Adams",
783 title = "Digitisation, Representation and Formalisation: Digital
784 Libraries of Mathematics.",
785 editor = "A. Asperti, B. Buchberger, J.H. Davenport",
786 booktitle = "Proceedings of Mathematical Knowledge Management 2003",
787 volume = "LNCS, 2594",
789 publisher = "Springer-Verlag",
794 author = "Serge Autexier and Dieter Hutter and Heiko Mantel and Axel Schairer",
795 title = "Towards an Evolutionary Formal Software-Development Using {CASL}",
796 booktitle = "WADT99 Selected Papers Volume",
797 volume = "LNCS, 1827",
798 publisher = "Springer-Verlag",
802 @inproceedings{how-to-extract,
803 author = "Lu\'is Cruz Filipe and Bas Spitters",
804 title = "Program Extraction from large proof developments",
805 booktitle = "Proceedings of TPHOLS 2003",
806 editor = "D. Basin and B. Wolff",
807 volume = "LNCS, 2758",
808 publisher = "Springer-Verlag",
812 @inproceedings{click-and-prove,
813 author = "Jean-Raymond Abrial and Dominique Cansell",
814 title = "Click'n {P}rove: Interactive Proofs Within Set Theory",
815 booktitle = "Proceedings of TPHOLS 2003",
816 editor = "D. Basin and B. Wolff",
817 volume = "LNCS, 2758",
818 publisher = "Springer-Verlag",
822 @inproceedings{delahaye,
823 author = "David Delahaye and Roberto di Cosmo",
824 title = "Information Retrieval in a {C}oq Proof Library using
826 booktitle = "Proceedings of TYPES 99",
828 publisher = "Springer-Verlag",
833 author = "G. I. Jojgov",
834 title = "Systems for open terms: An Overview",
835 institution = "Technische Universiteit Eindhoven",
836 number = "CSR 01-03",
840 @TechReport{garrigue:implicit-arguments,
841 author = "Jun P. Furuse and Jacques Garrigue",
842 title = " A label-selective lambda-calculus with optional arguments and its compilation method",
843 institution = "Research Institute for Mathematical Sciences, Kyoto University",
844 number = "RIMS Preprint 1041",
850 author = "Alexandre Miquel",
851 title = "Le {C}alcul des {C}onstructions {I}mplicite: syntaxe et s\'emantique",
852 school = "Universit\'e Paris 7",
856 @phdthesis{chrzaszcz,
857 author = "Jacek Chrz{\c{a}}szcs",
858 title = "Modules in Type Theory with Generative Definitions",
859 school = "Uniwersytet Warszawski and Universit\'e de Paris Sud",
864 author = "Olivier Pons",
865 title = "Conception et r\'ealisation d'outils d'aide au d\'eveloppement de grosse th\'eories dans les syst\`emes de preuves interactifs",
866 school = "Conservatoire National des Arts et M\'etiers",
871 author = "Fr\'ed\'eric Blanqui",
872 title = "Type Theory and Rewriting",
873 school = "Universit\'e Paris XI",
877 @phdthesis{magnusson,
878 author = "Lena Magnusson",
879 title = "The Implementation of {ALF} -- a Proof Editor based
880 on Martin-L{\"o}f Monomorphic Type Theory with Explicit
882 school = "Chalmers University of Technology / G{\"o}teborg University",
887 author = "Conor McBride",
888 title = "Dependently Typed Functional Programs and their Proofs",
889 school = "University of Edinburgh",
894 author = "Irene Schena",
895 title = "Towards a Semantic Web for Formal Mathematics",
896 school = "University of Bologna",
901 author = "Ferruccio Guidi",
902 title = "Searching and Retrieving in Content-Based Repositories
903 of Formal Mathematical Knowledge",
904 school = "University of Bologna",
907 note = "Technical Report UBLCS 2003-06"
911 author = "Luca Padovani",
912 title = "MathML Formatting",
913 school = "University of Bologna",
916 note = "Technical Report UBLCS 2003-03"
919 @mastersthesis{csc-master,
920 author = "Claudio {Sacerdoti Coen}",
921 title = "Progettazione e realizzazione con tecnologia {XML} di basi distribuite di conoscenza matematica formalizzata",
922 school = "University of Bologna",
926 @mastersthesis{zack-master,
927 author = "Stefano Zacchiroli",
928 title = "Web {s}ervices per il supporto alla dimostrazione interattiva",
929 school = "University of Bologna",
933 @mastersthesis{dilena,
934 author = "Pietro Dilena",
935 title = "Generazione automatica di stylesheet per notazione matematica",
936 school = "University of Bologna",
941 author = "C\'esar Munoz",
942 title = "A Calculus of Substitutions for Incomplete-Proof
943 Representation in Type Theory",
950 author = "Martin Strecker",
951 title = "Construction and Deduction in Type Theories",
952 school = "Universit{\"a}t Ulm",
956 @misc{content-centric,
957 author = "Andrea Asperti and Luca padovani
958 and Claudio {Sacerdoti Coen} and irene Schena",
959 title = "Content-centric Logical Envirnoments",
960 howpublished = "Short Presentation at the Fifteenth IEEE Symposium on Logic in Computer Science",
963 key = "content centric"
966 @misc{mowgli-proposal,
967 title = "The {MoWGLI Proposal}, {HTML} Version",
968 howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/project.html}",
969 key = "MoWGLI Proposal"
972 @misc{debrujinfactor,
973 title = "The ``de Bruijn factor''",
974 howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}",
976 author = "Freek Wiedijk",
979 @misc{mowgli-deliverables,
980 title = "{MoWGLI} Project Deliverables",
981 howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html}",
982 key = "MoWGLI Deliverables"
986 title = "The {ALF} family of proof-assistants",
987 howpublished = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
988 url = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
993 title = "The {C}oq Proof Assistant Reference Manual",
994 author = "{The Coq Development Team}",
995 howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
1001 title = "The {C}oq proof-assistant",
1002 howpublished = "\\\url{http://coq.inria.fr}",
1007 title = "The {PhoX} proof-assistant",
1008 howpublished = "\\\url{http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html}",
1013 title = "The {L}ego proof-assistant",
1014 howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}",
1019 title = "The {A}lfa proof editor",
1020 howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
1021 url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
1026 title = "The {PVS} Specification and Verification System",
1027 howpublished = "\\\url{http://pvs.csl.sri.com/}",
1032 title = "The {Isabelle} proof-assistant",
1033 howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}",
1038 author = "Constable, Robert L. and Stuart F. Allen and H. M. Bromley and
1039 W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and
1040 T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
1042 title = "Implementing Mathematics with the {N}uprl Development System",
1043 publisher = "Prentice-Hall",
1049 title = "The {NuPRL} proof-assistant",
1050 howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
1055 title = "The {HOL Light} proof-assistant",
1056 howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}",
1061 title = "The {MONET} project",
1062 howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}",
1067 title = "The {CALCULEMUS} project",
1068 howpublished = "\url{http://www.calculemus.net/}",
1069 url = "\url{http://www.calculemus.net/}",
1074 title = "The {M}izar proof-assistant",
1075 howpublished = "\\\url{http://mizar.uwb.edu.pl/}",
1080 howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium",
1081 author = "O. Caprotti and D. P. Carlisle and A. M. Cohen",
1082 title = "{\emph{The {O}pen{M}ath {S}tandard}}"
1086 title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
1087 editor="{Patrick Ion} and others",
1088 howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
1090 url = "\url{http://www.w3.org/TR/MathML2}",
1095 title = "{E}xtensible {M}arkup {L}anguage ({XML}). {V}ersion 1.0.",
1096 editor="{Tim Bray} and others",
1097 howpublished = "W3C Recommendation 10 February 1998,
1098 \url{http://www.w3.org/TR/REC-xml}",
1099 url = "\url{http://www.w3.org/TR/REC-xml}",
1104 title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0",
1105 howpublished = "W3C Candidate Recommendation 10 May 2000,
1106 \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1107 url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1112 title = "Universal Resource Identifiers in {WWW}",
1113 howpublished = "RFC 1630, CERN",
1120 title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0",
1121 howpublished = "W3C Recommendation, 16 November 1999,
1122 \url{http://www.w3.org/TR/xpath}",
1123 url = "\url{http://www.w3.org/TR/xpath}",
1128 title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0",
1129 howpublished = "W3C Recommendation, 16 November 1999,
1130 \url{http://www.w3.org/TR/xslt}",
1131 url = "\url{http://www.w3.org/TR/xslt}",
1136 title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax
1138 howpublished = "W3C Recommendation 22 February 1999,
1139 \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1140 url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1145 title = "{OMDoc}: An Open Markup Format for Mathematical Documents
1146 (Draft, Version 1.2)",
1147 howpublished = "\\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.2.pdf}",
1153 title = "The {F}ormavie project",
1154 howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1155 url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1160 title = "The {HELM} project",
1161 howpublished = "\url{http://helm.cs.unibo.it}",
1162 url = "\url{http://helm.cs.unibo.it}",
1167 title = "The {HELM} On-Line Library",
1168 howpublished = "\url{http://helm.cs.unibo.it/library.html}",
1169 url = "\url{http://helm.cs.unibo.it/library.html}",
1170 key = "HELM Library"
1174 title = "The {M}ath{W}eb project",
1175 howpublished = "\url{http://www.mathweb.org}",
1176 url = "\url{http://www.mathweb.org}",
1181 title = "The {PC}oq project",
1182 howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1183 url = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1188 author = "Andrea Asperti and Luca Padovani and Claudio {Sacerdoti Coen}
1190 title = "Towards a library of formal mathematics",
1192 note = "Panel session of the 13th {I}nternation {C}onference on
1193 {T}heorem {P}roving in {H}igher {O}rder {L}ogics
1194 ({TPHOLS}'2000), Portland, Oregon, USA",
1197 @inproceedings{Ring,
1198 author = "Samuel Boutin",
1199 title = "Using Reflection to Build Efficient and Certified Decision
1201 editor = "Martin Abadi and Takahashi Ito editors",
1202 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1205 publisher = "Springer-Verlag",
1209 @inproceedings{werner-zfc,
1210 author = "Benjamin Werner",
1211 title = "Sets in Types, Types in Sets",
1212 editor = "Martin Abadi and Takahashi Ito editors",
1213 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1216 publisher = "Springer-Verlag",
1221 author = "Peter Aczel",
1222 title = "On Relating Type Theories and Set Theories",
1223 journal = "Lecture Notes in Computer Science",
1228 @inproceedings{remathematization,
1229 author = "Andrea Asperti and Luca Padovani
1230 and Claudio {Sacerdoti Coen} and Irene Schena",
1231 title = "{XML}, Stylesheets and the re-mathematization
1233 booktitle = "Electronic Proceedings of {EXTREME Markup Languages} 2001",
1238 @phdthesis{YANNTHESIS,
1239 author = "Yann Coscoy",
1240 title = "Explication textuelle de preuves pour le {C}alcul des
1241 {C}onstructions {I}nductives",
1242 school = "Universit\'e de Nice-Sophia Antipolis",
1247 author = "Sylvain Lippi",
1248 title = "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)",
1249 school = "Universit\'e Aix-Marseille 2",
1254 author = "Benjamin Werner",
1255 title = "Une Th\'eorie des {C}onstructions {I}nductives",
1256 school = "Universit\'e Paris VII",
1261 @InCollection{Felleisen87,
1262 author = "M. Felleisen and D. Friedman",
1263 editor = "M. Wirsing",
1264 title = "Control operators, the {SECD}-machine, and the lambda calculus",
1265 booktitle = "Formal Description of Programming Concepts III",
1267 publisher = "Elsevier Science Publishers B.V.",
1268 address = "(North-Holland) Amsterdam",
1273 author = "Jan Zwanenburg",
1274 institution = "Eindhoven University of Technology",
1275 number = "Computing Science Report CS-98-11",
1276 title = "The Proof-assistant Yarrow",
1280 @TechReport{Ager2003a,
1281 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1282 institution = "BRICS",
1284 number = "BRICS RS-03-13",
1285 title = "A Functional Correspondence between Evaluators and Abstract Machines",
1289 @TechReport{Ager2003b,
1290 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1291 institution = "BRICS",
1293 number = "BRICS RS-03-14",
1294 title = "From Interpreter to Compiler and Virtual Machine: A Functional Derivation",
1298 @article{harperpollack,
1299 author = "Robert Harper and Robert Pollack",
1300 title = "Type checking with universes",
1301 journal = "Theoretical Computer Science",
1307 @article{activemath,
1308 author = "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich",
1309 title = "Knowledge Representation and Management in {ActiveMath}",
1310 journal = "Annals of Mathematics and Artificial Intelligence",
1318 author = "Andrea Asperti and Ferruccio Guidi and Luca Padovani and
1319 Claudio {Sacerdoti Coen} and Irene Schena",
1320 title = "Mathematical Knowledge Management in {HELM}",
1321 journal = "Annals of Mathematics and Artificial Intelligence",
1328 @unpublished{formal-topology,
1329 author = "Giovanni Sambin",
1330 title = "Some points in formal topology",
1331 note = "To appear in Theoretical Computer Science",
1335 @TechReport{JohnHarrison:complexity-of-floating-point-proofs,
1336 author = "John Harrison",
1337 title = "Real Numbers in Real Applications",
1338 note = "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002",
1339 institution = "NASA",
1340 number = "NASA/CP-2002-211736",
1344 @inproceedings{kohlhase-anghelache,
1345 author = "Michael Kohlhase and Romeo Anghelache",
1346 title = "Towards Collaborative Content Management And Version Control For
1347 Structured Mathematical Knowledge",
1348 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
1349 booktitle = "Proceedings of the Second International Conference on
1350 Mathematical Knowledge Management, MKM 2003",
1352 volume = "LNCS, 2594",
1353 publisher = "Springer-Verlag",
1357 %%% Unused entries from my Master dissertation bibliography
1360 title="{Standard Generalized Markup Language (SGML)}",
1361 note="ISO 8879:1986",
1366 author = "Andrea Asperti and Luca Padovani
1367 and Claudio {Sacerdoti Coen} and Irene Schena",
1368 title = "{Content Centric Logical Environments}",
1369 note = "Short Presentation at LICS 2000",
1370 ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz",
1374 author = "Andrea Asperti and Luca Padovani
1375 and Claudio {Sacerdoti Coen} and Irene Schena",
1376 title = "{Formal Mathematics in MathML}",
1377 note = "To be presented at MathML International Conference 2000",
1381 author = "Andrea Asperti and Luca Padovani
1382 and Claudio {Sacerdoti Coen} and Irene Schena",
1383 title = "{Towards a Library of Formal Mathematics}",
1384 note = "Accepted at TPHOLS 2000",
1385 ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz",
1388 @techreport{mowgli:D4a,
1389 author = "Hanane Naciri and Luca Padovani",
1390 title = "{MathML} Rendering/Browsing Engine",
1391 type = {MoWGLI Report},
1394 howpublished = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}"
1397 @techreport{hazewinkel,
1398 author = "Michiel Hazewinkel",
1399 title = "Dynamic stochastic models for indexes and thesauri,
1400 identification clouds, and information retrieval and
1402 type = "{MKM Net Report}",
1403 howpublished = "\url{http://monet.nag.co.uk/mkm//index.html}"
1406 @techreport{BarrasB:coqpar,
1407 author = "{Barras B.} and {Boutin S.} and {Cornes C.}
1408 and {Courant J.} and {Filliatre J. C.}
1409 and {Gim\'enez E.} and {Herbelin H.} and {Huet G.}
1410 and {Munoz C.} and {Murthy C.} and {Parent C.}
1411 and {Paulin-Mohring C.} and {Saibi A.}
1413 title = "{The Coq Proof Assistant Reference Manual : Version
1415 institution = {Inria (Institut National de Recherche en Informatique
1416 et en Automatique), France},
1417 type = {Technical Report},
1420 author_acronym = {WernerB},
1421 bibdate = {May 1, 1997},
1422 source = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/},
1423 source-date = {Mon 11 Sep 100},
1424 title_acronym = {coqpar}
1427 @unpublished{bw:1997,
1428 author = "Bruno Barras and Benjamin Werner",
1429 title = "{Coq in Coq}",
1432 ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz",
1435 @unpublished{berners-lee:1989,
1436 author = "Tim Berners-Lee",
1437 title = "{Information Management: A Proposal}",
1439 ps = "http://www.w3.org/History/1989/proposal.html",
1442 @techreport{natural,
1443 author = "Yann Coscoy and Gilles Kahn and Laurent Thery",
1444 title = "{Extracting Text from Proofs}",
1445 institution = {Inria (Institut National de Recherche en Informatique
1446 et en Automatique), France},
1447 type = {Technical Report},
1452 @inproceedings{Bru80,
1453 author = "de Bruijn, N. G.",
1454 title = "{A survey of the project AUTOMATH}",
1456 editor = "J. P. Seldin and J. R. Hindley",
1457 booktitle = "To H. B. Curry: Essays in Combinatory Logic,
1458 Lambda Calculus and Formalism",
1460 publisher = "Academic Press"
1463 @techreport{tutrect,
1464 author = "E Gim\'enez",
1465 title = "{A Tutorial on Recursive Types in Coq}",
1466 institution = {Inria (Institut National de Recherche en Informatique
1467 et en Automatique), France},
1468 type = {Technical Report},
1474 author = "John Harrison",
1475 title = "{The QED Manifesto}",
1477 booktitle = "Automated Deduction - CADE 12",
1478 series = "Lecture Notes in Artificial Intelligence",
1481 publisher = "Springer-Verlag"
1484 @inproceedings{harrison-mizar,
1485 author = "John Harrison",
1486 title = "{A Mizar Mode for HOL}",
1488 editor = "Joakim von Wright and Jim Grundy and John Harrison",
1489 booktitle = "Theorem Proving in Higher Order Logics:
1490 9th International Conference, TPHOLs'96",
1491 series = "Lecture Notes in Computer Science",
1493 address = "Turku, Finland",
1494 date = "26--30 August 1996",
1496 publisher = "Springer-Verlag"
1499 @inproceedings{proverb,
1500 author="H. Horacek",
1501 title="{Presenting Proofs in a Human Oriented Way}",
1502 booktitle="16th International Conference on Automated Deduction",
1507 author = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring",
1508 title = "{The Coq Proof Assistant. A Tutorial}",
1513 author="{Jutting van L. S. B.}",
1514 school = {{Eindhoven University of Technology}},
1515 title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}",
1516 type = {Ph D. thesis},
1517 note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}",
1521 @misc{abriefhistoryoftheinternet,
1522 author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.}
1523 and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.}
1524 and {Postel J.} and {Roberts L. G.} and {Wolff S.}",
1525 title="{A Brief Hystory of the Internet}",
1526 note="http://www.isoc.org/internet-history/brief.html"
1529 @inproceedings{MacKenzie:1995,
1530 author="{MacKenzie D.}",
1531 title="{The automation of proof: A historical and sociological exploration}",
1532 booktitle="IEEE: Annals of the History of Computing",
1537 author = "Christine Paulin-Mohring",
1539 school = {{Paris 7}},
1540 title = "{Extraction de programmes dans le Calcul des Constructions}",
1541 type = {Th\`ese d'universit\'e},
1543 url = {http://www.lri.fr/~paulin/these.ps.gz},
1547 author = "A. Ricci",
1548 school = {{Universit\`a degli studi di Bologna}},
1549 title = "{Studio e progettazione di un modello RDF per biblioteche matematiche
1551 type = {Tesi universitaria},
1555 @inproceedings{Rob65,
1556 author="{Robinson J. A.}",
1557 title = "{A machine-oriented logic based on the resolution principle}",
1559 booktitle = "Journal of the ACM",
1564 @inproceedings{sh:1995,
1565 author="{Saibi A.} and {Huet G.}",
1566 title="{Constructive Category Theory}",
1567 booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory",
1568 address="Goteborg (Sweden)",
1573 @inproceedings{ranta2,
1574 author="Thomas Hallgren and Aarne Ranta",
1575 title="An extensible proof text editor",
1576 BOOKTITLE = {LPAR'2000},
1577 SERIES = {LNCS/LNAI},
1582 @inproceedings{werner:1997,
1583 author="Benjamin Werner",
1584 title="{Constructive Category Theory}",
1585 booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software",
1589 @inproceedings{barthe95implicit,
1590 author = "Gilles Barthe",
1591 title = "Implicit Coercions in Type Systems",
1592 booktitle = "Types for Proofs and Programs: International Workshop, {TYPES 1995}",
1595 url = "citeseer.ist.psu.edu/barthe95implicit.html" }