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