2 @inproceedings{gmetadom,
3 author = "Luca Padovani and Claudio Sacerdoti Coen and Stefano Zacchiroli",
4 title = "A Generative Approach to the Implementation of Language Bindings for the Document Object Model",
5 booktitle = "Generative Programming and Component Engineering",
6 editor = "Gabor Karsai and Eelco Visser",
10 publisher = "Springer-Verlag",
15 author = "Freek Wiedijk",
16 title = "MMode, a Mizar Mode for the proof assistant Coq",
17 institution = "University of Nijmegen",
18 number = "NIII-R0333",
22 @article{ lamport-proof,
23 author = "Leslie Lamport",
24 title = "How to write a proof",
25 journal = "American Mathematical Monthly",
32 @inproceedings{thery-authoring,
33 author = "Laurent Th\`ery",
34 title = "Formal Proof Authoring: an Experiment",
35 booktitle = "User Interface Design for Theorem Provers",
36 editor = "David Aspinall and Christoph L{\"u}th",
40 @inproceedings{padovani-editex,
41 author = "Luca Padovani",
42 title = "Interactive Editing of MathML Markup Using TeX Syntax",
43 booktitle = "International Conference on TeX, XML, and Digital Typography",
48 publisher = "Springer-Verlag",
51 @inproceedings{uitp-knowledge-modelling,
52 author = "Stuart Aitken",
53 title = "Problem Solving in Interactive Proof: A Knowledge-Modelling Approach",
54 booktitle = "European Conference on Artificial Intelligence (ECAI)",
58 @inproceedings{proof-by-pointing,
59 author = "Yves Bertot",
60 title = "Proof by Pointing",
61 booktitle = "Symposium on Theoretical Aspects Computer Software (STACS)",
62 series = "Lecture Notes in Computer Science",
67 @inproceedings{thery-cyp,
68 author = "Laurent Th\`ery",
69 title = "Colouring proofs: a lightweight approach to adding formal structure to proofs",
70 booktitle = "User Interface Design for Theorem Provers",
71 editor = "David Aspinall and Christoph L{\"u}th",
75 @article{uitp-empirical,
76 author = "Stuart Aitken and Phil Gray and Tom Melham and Muffy Thomas",
77 title = "Interactive Theorem Proving: An Empirical Study of User Activity",
78 journal = "Journal of Symbolic Computation",
82 @inproceedings{uitp-phases,
83 author = "Stuart Aitken and Phil Gray and Tom Melham and Muffy Thomas",
84 title = "Phases, Modes and Information Flow in Theory Development",
85 booktitle = "User Interface Design for Theorem Provers",
86 editor = "Nicholas Merriam",
90 @inproceedings{searchingmath,
91 author = "Andrea Asperti and Stefano Zacchiroli",
92 title = "Searching mathematics on the Web: state of the art and future developments",
93 booktitle = "New Developments in Electronic Publishing of Mathematics",
94 editor = "Bernd Wegner",
95 publisher = {FIZ Karlsruhe},
100 author = "K. Appel and W. Haken",
101 title = "Every planar map is four colorable.",
102 journal = {Illinois Journal of Mathematics},
108 @misc{freekcomparison,
109 author = "Freek Wiedijk",
110 title = "The Sixteen Provers of the World",
111 howpublished = "University of Nijmegen,\\\url{http://www.cs.ru.nl/~freek/comparison/comparison.ps.gz}"
115 title = "Zentralblatt MATH",
116 howpublished = "\url{http://www.emis.de/ZMATH/}"
120 author = "Michael J. C. Gordon and Robin Milner and C.P. Wadsworth",
121 title = "{Edinburgh LCF}: a Mechanised Logic of Computation",
122 series = {Lecture Notes in Computer Science},
124 publisher = {{Sprin\-ger-Verlag}},
129 author = "Claudio Sacerdoti Coen",
130 title = "Mathematical Knowledge Management and Interactive Theorem
132 school = "University of Bologna",
134 note = "Technical Report UBLCS 2004-5"
138 author = "Markus Wenzel",
139 title = "Isar - A Generic Interpretative Approach to Readable Formal Proof Documents",
140 booktitle = "Theorem Proving in Higher Order Logics",
145 @inproceedings{centaur,
146 author = "P. Borras and D. Clement and Th. Despeyrouz and J. Incerpi and G. Kahn and B. Lang and V. Pascual",
147 title = "{CENTAUR}: The System",
148 booktitle = "Proceedings of the {ACM} {SIGSOFT}/{SIGPLAN} Software Engineering Symposium on Practical Software Development Environments ({PSDE})",
149 journal = "SIGPLAN Notices",
152 publisher = "ACM Press",
153 address = "New York, NY",
156 url = "citeseer.nj.nec.com/borras88centaur.html"
159 @inproceedings{Leroy-manifest-types,
160 AUTHOR = "Xavier Leroy",
161 TITLE = "Manifest types, modules, and separate compilation",
162 BOOKTITLE = {21st symposium Principles of Programming Languages},
164 PUBLISHER = {ACM Press},
166 URL = {http://pauillac.inria.fr/~xleroy/publi/manifest-types-popl.ps.gz}
169 @inproceedings{overkilling,
170 author = "Sacerdoti Coen, Claudio",
171 title = "Tactics in Modern Proof-Assistants: the Bad Habit of
173 booktitle = "Supplementary Proceedings of the 14th International
174 Conference TPHOLS 2001",
179 @inproceedings{omegaants1,
180 author = "Christoph Benzm{\"u}ller and Volker Sorge",
181 title = {{OANTS} -- An open approach at combining Interactive and Automated
183 booktitle = {Symbolic Computation and Automated Reasoning},
184 editor = {Manfred Kerber and Michael Kohlhase},
187 publisher = {A.K.Peters},
188 url = {www.ags.uni-sb.de/~chris/papers/C8.pdf}
192 author = "R. Fateman and T. Tokuyasu and B. Berman and N. Mitchell",
193 title = {Optical Character Recognition and Parsing of Typeset Mathematics},
194 journal = {Journal of Visual Communication And Image Representation},
200 url = {www.ags.uni-sb.de/~chris/papers/J4.pdf}
203 @article{newauthomath,
204 author = "Freek Wiedijk",
205 title = "A new implementation of {A}utomath",
206 journal = {Journal of Automated Reasoning},
213 author = "Paolo Casarini and Luca Padovani",
214 title = "The {G}nome {DOM} {E}ngine",
215 journal = "Markup Languages: Theory \& Practice",
220 publisher = "MIT Press",
225 author = "Christoph Benzm{\"u}ller and Mateja Jamnik and Manfred Kerber and
227 title = {Agent based Mathematical Reasoning},
228 journal = {Electronic Notes in Theoretical Computer Science, Elsevier},
233 url = {www.ags.uni-sb.de/~chris/papers/J4.pdf}
236 @inproceedings{Necula,
237 author = "George C. Necula and Peter Lee",
238 title = "Safe Kernel Extensions Without Run-Time Checking",
239 booktitle = "2nd Symposium on Operating Systems Design and Implementation ({OSDI} '96), October 28--31, 1996. Seattle, {WA}",
240 publisher = "USENIX",
241 address = "Berkeley, CA, USA",
245 url = "citeseer.nj.nec.com/necula96safe.html"
248 @inproceedings{courant,
249 AUTHOR = "Judica{\"e}l Courant",
250 TITLE = {Explicit Universes for the {C}alculus of {C}onstructions},
251 BOOKTITLE = {Theorem Proving in Higher Order Logics:
252 15th International Conference, TPHOLs 2002},
253 EDITOR = {Victor A. {Carre\~{n}o} and C\'{e}sar A. {Mu\~{n}oz} and Sofi\`{e}ne Tahar},
254 SERIES = {Lecture Notes in Computer Science},
258 PUBLISHER = {{Sprin\-ger-Verlag}},
260 ADDRESS = {Hampton, VA, USA}
264 author = "George C. Necula and Peter Lee",
265 title="{Efficient Representation and Validation of Proofs}",
266 booktitle="Proceedings of the 13th Annual symposium on Logic in Computer Science,",
267 address="Indianapolis",
272 author = "Jean-Yves Girard and Yves Lafont and Paul Taylor",
273 title = "{Proofs and Types}",
274 publisher = {Cambridge University Press},
275 series = {Cambridge Tracts in Theoretical Computer Science},
279 @inproceedings{proofgeneral,
280 author = "David Aspinall",
281 title = "{P}roof {G}eneral: A Generic Tool for Proof Development",
282 booktitle = "Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000",
287 publisher = "Springer-Verlag",
290 @inproceedings{Gim94,
291 author = "Eduardo Gim\'enez",
292 title = "{Codifying guarded definitions with recursive schemes}",
293 booktitle = "Types'94: Types for Proofs and Programs",
297 publisher = "Springer-Verlag",
298 note = "Extended version in LIP research report 95-07, ENS Lyon",
302 @incollection{BarendregtH:lawcwt,
303 author = "H. Barendregt",
304 title = "{Lambda Calculi with Types}",
305 booktitle = "{Handbook of Logic in Computer Science}",
306 editor = "{Abramsky, Samson and others}",
307 publisher = "{Oxford University Press}",
312 @inproceedings{coquand:1986,
313 author="Thierry Coquand",
314 title="{An Analysis of Girard's Paradox}",
315 booktitle="Symposium on Logic in Computer Science",
317 publisher="MA. IEEE press",
322 AUTHOR = "Christine Paulin-Mohring",
323 TITLE = {D\'efinitions Inductives en Th\'eorie des Types d'Ordre Sup\'rieur},
324 SCHOOL = {Universit\'e Claude Bernard Lyon I},
327 TYPE = {Habilitation \`a diriger les recherches},
328 URL = {http://www.lri.fr/~paulin/habilitation.ps.gz}
332 author = "Jacques Garrigue",
333 title = "{Label-Selective Lambda-Calculi and Transformation Calculi}",
334 school = "University of Tokyo, Department of Information Science",
339 @phdthesis{LuoZ:extcc,
340 author = "Zhaohui Luo",
341 title = "{An Extended Calculus of Constructions}",
342 school = "University of Edinburgh",
347 author = "Laurent Chicli",
348 title = "Sur la formalisation des math\'ematiques dans le
349 {C}alcul des {C}onstructions {I}nductives",
350 school = "Universit\'e de Nice~-~Sophia Antipolis",
354 @phdthesis{geuvers:1993,
355 author="Herman Geuvers",
356 title="{Logics and Type Systems}",
357 school="Catholic University Nijmegen",
359 type="{Ph.D.} dissertation"
362 @unpublished{PrimesInP,
363 author = "M. Agrawal and N. Kayal and N. Saxena",
364 title = "{PRIMES} in {P}",
365 note = "\url{http://www.cse.iitk.ac.in/users/manindra/primality.ps}",
370 @unpublished{danosKAM,
371 author = "Vincent Danos and Laurent Regnier",
372 title = "How abstract machines implement head linear reduction",
376 @inproceedings{Oostdijk,
377 author = "Olga Caprotti and Herman Geuvers and Martin Oostdijk",
378 title = "Certified and Portable Mathematical Documents from Formal Contexts",
379 editor = "Bruno Buchberger and Olga Caprotti",
380 booktitle = "On-Line Proceedings of the First International Conference on
381 Mathematical Knowledge Management, MKM 2001",
382 publisher = "The Electronic Library of Mathematics (EMIS)",
383 url = "\url{http://www.emis.de/ELibM.html}",
387 @inproceedings{formal-proof-sketches,
388 author = "Freek Wiedijk",
389 title = "Formal Proof Sketches",
390 editor = "Wan Fokkink and Jaco van de Pol",
391 booktitle = "7th Dutch Proof Tools Day, Program + Proceedings",
392 note = "CWI, Amsterdam",
396 @inproceedings{Barendregt,
397 author = "Henk Barendregt",
398 title = "Towards an Interactive Mathematical Proof Language",
399 editor = "Fairouz Kamareddine",
400 booktitle = "Thirty Five Years of Automath",
402 publisher = "Kluwer",
406 @inproceedings{werner:prof-irrelevance,
407 author = "Alexandre Miquel and Benjamin Werner",
408 title = "The Not So Simple Proof-Irrelevant Model of {CC}",
409 editor = "Herman Geuvers and Freek Wiedijk",
410 booktitle = "Types for Proofs and Programs: International Workshop, TYPES 2002",
412 volume = "LNCS, 2646",
413 publisher = "Springer-Verlag",
417 @inproceedings{csc-environment,
418 author = "Claudio Sacerdoti Coen",
419 title = "Mathematical Libraries as Proof Assistant Environments",
420 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
421 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
422 volume = "LNCS, 3119",
424 publisher = "Springer-Verlag",
428 @inproceedings{disambiguation,
429 author = "Claudio Sacerdoti Coen and Stefano Zacchiroli",
430 title = "Efficient Ambiguous Parsing of Mathematical Formulae",
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{pechino,
440 author = "Andrea Asperti and Bernd Wegner",
441 title = "An Approach to Machine-Understandable Representation of the Mathematical Information in Digital Documents",
442 editor = "Fengshai Bai and Bernd Wegner",
443 booktitle = "Electronic Information and Communication in Mathematics",
444 volume = "LNCS, 2730",
446 publisher = "Springer-Verlag",
450 @inproceedings{whelp,
451 author = "Andrea Asperti and Ferruccio Guidi and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli",
452 title = "A content based mathematical search engine: Whelp",
453 booktitle = "Post-proceedings of the Types 2004 International Conference",
454 volume = "LNCS, (to appear)",
456 publisher = "Springer-Verlag",
460 @inproceedings{exportation-module,
461 author = "Sacerdoti Coen, Claudio",
462 title = "From Proof-Assistans to Distributed Libraries of Mathematics: Tips
464 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
465 booktitle = "Proceedings of the Second International Conference on
466 Mathematical Knowledge Management, MKM 2003",
468 volume = "LNCS, 2594",
469 publisher = "Springer-Verlag",
474 author = "Andrea Asperti and Herman Geuvers and Iris Loeb and Lionel Elie Mamane and Claudio Sacerdoti Coen",
475 title = "An Interactive Algebra Course with Formalised Proofs and Definitions",
476 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
477 booktitle = "Post-Proceedings of the Fourth International Conference on Mathematical Knowledge Management, MKM 2005",
479 volume = "LNCS, (to appear)",
480 publisher = "Springer-Verlag",
484 @inproceedings{davenport,
485 author = "James H. Davenport",
486 title = "{MKM} from Book to Computer: A Case Study",
487 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
488 booktitle = "Proceedings of the Second International Conference on
489 Mathematical Knowledge Management, MKM 2003",
491 volume = "LNCS, 2594",
492 publisher = "Springer-Verlag",
496 @inproceedings{fguidisacerdot,
497 author = "Ferruccio Guidi and Sacerdoti Coen, Claudio",
498 title = "Querying Distributed Digital Libraries of Mathematics",
499 editor = "Therese Hardin and Renaud Rioboo",
500 booktitle = "Calculemus 2003",
502 publisher = "Aracne Editrice S.R.L.",
504 note = "ISBN 88-7999-545-6"
507 @inproceedings{hbugs,
508 author = "Sacerdoti Coen, Claudio and Stefano Zacchiroli",
509 title = "Brokers and {W}eb-Services for Automatic Deduction: a Case Study",
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{calculemus-presentation,
519 author = "Christoph Benzm{\"u}ller",
520 title = "The {CALCULEMUS} Research Training Network -- A short Overview",
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{linda,
530 author = "Sacerdoti Coen, Claudio",
531 title = "A Constructive Proof of the Soundness of the
532 Encoding of Random Access Machines in a Linda Calculus with Ordered
534 booktitle = "Theoretical Computer Science: 8th Italian Conference, ICTCS 2003",
536 volume = "LNCS, 2841",
537 publisher = "Springer-Verlag",
542 @article{asperti-categorical-understanding,
543 author = "Andrea Asperti",
544 title = "A categorical understanding of environment machines",
545 journal = "Journal of Functional Programming",
553 @article{namelessdummies,
554 author = "{N. G. de Bruijn}",
555 title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem",
556 journal = "Indagationes Mathematicae",
563 author = "Yves Bertot",
564 title = "The CtCoq System: Design and Architecture",
565 journal = "Formal Aspects of Computing",
572 author = "Yves Bertot and Laurent Th\'ery",
573 title = "A Generic Approach to Building User Interfaces for Theorem Provers",
574 journal = "Journal of Symbolic Computation",
581 author = "Michael Kohlhase and Andreas Franke",
582 title = "{MBase}: Representing Knowledge and Context for the Integration of Mathematical Software Systems",
583 journal = "Journal of Symbolic Computation",
588 url = "\url{http://citeseer.nj.nec.com/kohlhase00mbase.html}"
591 @inproceedings{mizarql,
592 author = "Grzegorz Bancerek and Piotr Rudnicki",
593 title = "Information Retrieval in {MML}",
594 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
595 booktitle = "Proceedings of the Second International Conference on
596 Mathematical Knowledge Management, MKM 2003",
598 volume = "LNCS, 2594",
599 publisher = "Springer-Verlag",
603 @article{codedcontexttrees,
604 author = "Harald Ganzinger and Robert Nieuwehuis and Pilar Nivela",
605 title = "Fast Term Indexing with Coded Context Trees. Journal of Automated Reasoning",
606 journal = "Journal of Automated Reasoning",
611 author = "Aarne Ranta",
612 title = "Grammatical Framework: A Type-Theoretical Grammar Formalism",
613 journal = "Journal of Functional Programming",
615 note = "Manuscript made available in September 2002"
619 AUTHOR = "Di Cosmo, Roberto",
620 TITLE = {Isomorphisms of types: from $\lambda$-calculus to information retrieval and language design},
621 SERIES = {Progress in Theoretical Computer Science},
622 PUBLISHER = {Birkhauser},
624 NOTE = {ISBN-0-8176-3763-X}
628 EDITOR = "R.P. Nederpelt and J.H. Geuvers and R.C. de Vrijer",
629 TITLE = {Selected Papers on Automath},
630 SERIES = {Studies in Logic and the Foundations of Mathematics},
631 PUBLISHER = {Elsevier Science},
634 NOTE = {ISBN-0444898220}
638 author = "Jean-Louis Krivine",
639 title = "Un interpr\`ete du $\lambda$-calcul",
640 howpublished = "Brouillon. Available on-line at \url{http://www.logique.jussieu.fr/~krivine}",
645 title = "Progress Report: Building Interactive Digital Libraries of Formal
646 Algorithmic Knowledge",
647 howpublished = "Cornell University, \url{http://www.cs.uwyo.edu/~nuprl/documents/cornell_slides.pdf}",
653 @misc{metadata4education,
654 title = "{L}earning {O}bject {M}etadata Standard",
655 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+",
660 @misc{openmath-cd-with-plus,
661 title = "Arith1 {OpenMath} {C}ontent {D}ictionary",
662 howpublished = "The OpenMath Society, \url{http://www.openmath.org/cocoon/openmath/cd/arith1.ocd}",
664 key = "Arith1 OpenMath Content Dictionary"
669 title = "Dewey Decimal Classification",
670 howpublished = "\url{http://www.oclc.org/dewey}",
671 url = "\url{http://www.oclc.org/dewey}",
676 title = "Library of Congress Classification Scheme",
677 howpublished = "\url{http://www.loc.gov}",
678 url = "\url{http://www.loc.gov}",
683 title = "Mathematical {S}ubject {C}lassification, {A}merican {M}athematical {S}ociety",
684 howpublished = "\url{http://www.ams.org/msc}",
685 url = "\url{http://www.ams.org/msc}",
689 @InCollection{borges,
690 author = "Jorge Luis Borges",
691 title = "The Library of {B}abel",
692 publisher = "Grove Press",
693 booktitle = "Ficciones",
697 @inproceedings{magaud,
698 author = "Nicolas Magaud",
699 title = "{C}hanging {D}ata {R}epresentation within the {C}oq {S}ystem",
700 booktitle = {TPHOLs'2003},
701 publisher = {Springer-Verlag},
702 volume = {LNCS, 2758},
706 @inproceedings{geuvers-jojgov,
707 author = "Herman Geuvers and Gueorgui I. Jojgov",
708 title = "Open Proofs and Open Terms: A Basis for Interactive Logic",
709 editor = "J. Bradfield",
710 booktitle = "Computer Science Logic: 16th International Workshop, CLS 2002",
712 volume = "LNCS, 2471",
713 publisher = "Springer-Verlag",
718 @inproceedings{mkm-structure,
719 author = "Koji Nakagawa and Akihiro Nomura and Masakazu Suzuki",
720 title = "Extraction of Logical Structure from articles in Mathematics",
721 editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
722 booktitle = "Proceedings of Mathematical Knowledge Management 2004",
723 volume = "LNCS, 3119",
725 publisher = "Springer-Verlag",
729 @inproceedings{mkm-metadata2,
730 author = "Andrea Asperti and Matteo Selmi",
731 title = "Efficient Retrieval of Mathematical Statements",
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{adams,
741 author = "A. A. Adams",
742 title = "Digitisation, Representation and Formalisation: Digital
743 Libraries of Mathematics.",
744 editor = "A. Asperti, B. Buchberger, J.H. Davenport",
745 booktitle = "Proceedings of Mathematical Knowledge Management 2003",
746 volume = "LNCS, 2594",
748 publisher = "Springer-Verlag",
753 author = "Serge Autexier and Dieter Hutter and Heiko Mantel and Axel Schairer",
754 title = "Towards an Evolutionary Formal Software-Development Using {CASL}",
755 booktitle = "WADT99 Selected Papers Volume",
756 volume = "LNCS, 1827",
757 publisher = "Springer-Verlag",
761 @inproceedings{how-to-extract,
762 author = "Lu\'is Cruz Filipe and Bas Spitters",
763 title = "Program Extraction from large proof developments",
764 booktitle = "Proceedings of TPHOLS 2003",
765 editor = "D. Basin and B. Wolff",
766 volume = "LNCS, 2758",
767 publisher = "Springer-Verlag",
771 @inproceedings{click-and-prove,
772 author = "Jean-Raymond Abrial and Dominique Cansell",
773 title = "Click'n {P}rove: Interactive Proofs Within Set Theory",
774 booktitle = "Proceedings of TPHOLS 2003",
775 editor = "D. Basin and B. Wolff",
776 volume = "LNCS, 2758",
777 publisher = "Springer-Verlag",
781 @inproceedings{delahaye,
782 author = "David Delahaye and Roberto di Cosmo",
783 title = "Information Retrieval in a {C}oq Proof Library using
785 booktitle = "Proceedings of TYPES 99",
787 publisher = "Springer-Verlag",
792 author = "G. I. Jojgov",
793 title = "Systems for open terms: An Overview",
794 institution = "Technische Universiteit Eindhoven",
795 number = "CSR 01-03",
799 @TechReport{garrigue:implicit-arguments,
800 author = "Jun P. Furuse and Jacques Garrigue",
801 title = " A label-selective lambda-calculus with optional arguments and its compilation method",
802 institution = "Research Institute for Mathematical Sciences, Kyoto University",
803 number = "RIMS Preprint 1041",
809 author = "Alexandre Miquel",
810 title = "Le {C}alcul des {C}onstructions {I}mplicite: syntaxe et s\'emantique",
811 school = "Universit\'e Paris 7",
815 @phdthesis{chrzaszcz,
816 author = "Jacek Chrz{\c{a}}szcs",
817 title = "Modules in Type Theory with Generative Definitions",
818 school = "Uniwersytet Warszawski and Universit\'e de Paris Sud",
823 author = "Olivier Pons",
824 title = "Conception et r\'ealisation d'outils d'aide au d\'eveloppement de grosse th\'eories dans les syst\`emes de preuves interactifs",
825 school = "Conservatoire National des Arts et M\'etiers",
830 author = "Fr\'ed\'eric Blanqui",
831 title = "Type Theory and Rewriting",
832 school = "Universit\'e Paris XI",
836 @phdthesis{magnusson,
837 author = "Lena Magnusson",
838 title = "The Implementation of {ALF} -- a Proof Editor based
839 on Martin-L{\"o}f Monomorphic Type Theory with Explicit
841 school = "Chalmers University of Technology / G{\"o}teborg University",
846 author = "Conor McBride",
847 title = "Dependently Typed Functional Programs and their Proofs",
848 school = "University of Edinburgh",
853 author = "Irene Schena",
854 title = "Towards a Semantic Web for Formal Mathematics",
855 school = "University of Bologna",
860 author = "Ferruccio Guidi",
861 title = "Searching and Retrieving in Content-Based Repositories
862 of Formal Mathematical Knowledge",
863 school = "University of Bologna",
866 note = "Technical Report UBLCS 2003-06"
870 author = "Luca Padovani",
871 title = "MathML Formatting",
872 school = "University of Bologna",
875 note = "Technical Report UBLCS 2003-03"
878 @mastersthesis{csc-master,
879 author = "Sacerdoti Coen, Claudio",
880 title = "Progettazione e realizzazione con tecnologia {XML} di basi distribuite di conoscenza matematica formalizzata",
881 school = "University of Bologna",
885 @mastersthesis{zack-master,
886 author = "Stefano Zacchiroli",
887 title = "Web {s}ervices per il supporto alla dimostrazione interattiva",
888 school = "University of Bologna",
892 @mastersthesis{dilena,
893 author = "Pietro Dilena",
894 title = "Generazione automatica di stylesheet per notazione matematica",
895 school = "University of Bologna",
900 author = "C\'esar Munoz",
901 title = "A Calculus of Substitutions for Incomplete-Proof
902 Representation in Type Theory",
909 author = "Martin Strecker",
910 title = "Construction and Deduction in Type Theories",
911 school = "Universit{\"a}t Ulm",
916 @misc{mowgli-proposal,
917 title = "The {MoWGLI Proposal}, {HTML} Version",
918 howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/project.html}",
919 key = "MoWGLI Proposal"
922 @misc{debrujinfactor,
923 title = "The ``de Bruijn factor''",
924 howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}",
925 author = "Freek Wiedijk",
928 @misc{mowgli-deliverables,
929 title = "{MoWGLI} Project Deliverables",
930 howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html}",
931 key = "MoWGLI Deliverables"
935 title = "The {ALF} family of proof-assistants",
936 howpublished = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
937 url = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
942 title = "The {C}oq Proof Assistant Reference Manual",
943 author = "The Coq Development Team",
944 howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
949 title = "The {C}oq proof-assistant",
950 howpublished = "\\\url{http://coq.inria.fr}",
955 title = "The {PhoX} proof-assistant",
956 howpublished = "\\\url{http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html}",
961 title = "The {L}ego proof-assistant",
962 howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}",
963 url = "\url{http://www.dcs.ed.ac.uk/home/lego/}",
968 title = "The {A}lfa proof editor",
969 howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
970 url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
975 title = "The {PVS} Specification and Verification System",
976 howpublished = "\\\url{http://pvs.csl.sri.com/}",
981 title = "The {Isabelle} proof-assistant",
982 howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}",
987 author = "Constable, Robert L. and Stuart F. Allen and H. M. Bromley and
988 W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and
989 T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
991 title = "Implementing Mathematics with the {N}uprl Development System",
992 publisher = "Prentice-Hall",
998 title = "The {NuPRL} proof-assistant",
999 howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
1004 title = "The {HOL Light} proof-assistant",
1005 howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}",
1010 title = "The {MONET} project",
1011 howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}",
1016 title = "The {CALCULEMUS} project",
1017 howpublished = "\url{http://www.calculemus.net/}",
1018 url = "\url{http://www.calculemus.net/}",
1023 title = "The {M}izar proof-assistant",
1024 howpublished = "\\\url{http://mizar.uwb.edu.pl/}",
1029 howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium",
1030 author = "O. Caprotti and D. P. Carlisle and A. M. Cohen",
1031 title = "{\emph{The {O}pen{M}ath {S}tandard}}"
1035 title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
1036 editor="{Patrick Ion} and others",
1037 howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
1038 url = "\url{http://www.w3.org/TR/MathML2}",
1039 key = "Mathematical"
1043 title = "{E}xtensible {M}arkup {L}anguage ({XML}). {V}ersion 1.0.",
1044 editor="{Tim Bray} and others",
1045 howpublished = "W3C Recommendation 10 February 1998,
1046 \url{http://www.w3.org/TR/REC-xml}",
1047 url = "\url{http://www.w3.org/TR/REC-xml}",
1052 title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0",
1053 howpublished = "W3C Candidate Recommendation 10 May 2000,
1054 \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1055 url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1060 title = "Universal Resource Identifiers in {WWW}",
1061 howpublished = "RFC 1630, CERN",
1068 title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0",
1069 howpublished = "W3C Recommendation, 16 November 1999,
1070 \url{http://www.w3.org/TR/xpath}",
1071 url = "\url{http://www.w3.org/TR/xpath}",
1076 title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0",
1077 howpublished = "W3C Recommendation, 16 November 1999,
1078 \url{http://www.w3.org/TR/xslt}",
1079 url = "\url{http://www.w3.org/TR/xslt}",
1084 title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax
1086 howpublished = "W3C Recommendation 22 February 1999,
1087 \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1088 url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1093 title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)",
1094 howpublished = "\\\url{http://www.mathweb.org/omdoc/omdoc.ps}",
1099 title = "The {F}ormavie project",
1100 howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1101 url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1106 title = "The {HELM} project",
1107 howpublished = "\url{http://helm.cs.unibo.it}",
1108 url = "\url{http://helm.cs.unibo.it}",
1113 title = "The {HELM} On-Line Library",
1114 howpublished = "\url{http://helm.cs.unibo.it/library.html}",
1115 url = "\url{http://helm.cs.unibo.it/library.html}",
1116 key = "HELM Library"
1120 title = "The {M}ath{W}eb project",
1121 howpublished = "\url{http://www.mathweb.org}",
1122 url = "\url{http://www.mathweb.org}",
1127 title = "The {PC}oq project",
1128 howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1129 url = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1134 author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen
1136 title = "Towards a library of formal mathematics",
1138 note = "Panel session of the 13th {I}nternation {C}onference on
1139 {T}heorem {P}roving in {H}igher {O}rder {L}ogics
1140 ({TPHOLS}'2000), Portland, Oregon, USA",
1144 author = "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
1145 title = "Real Theorem Provers Deserve Real User-Interfaces",
1148 institution = "INRIA",
1149 number = "{Inria Research Report 1684}"
1152 @inproceedings{Ring,
1153 author = "Samuel Boutin",
1154 title = "Using Reflection to Build Efficient and Certified Decision
1156 editor = "Martin Abadi and Takahashi Ito editors",
1157 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1160 publisher = "Springer-Verlag",
1164 @inproceedings{werner-zfc,
1165 author = "Benjamin Werner",
1166 title = "Sets in Types, Types in Sets",
1167 editor = "Martin Abadi and Takahashi Ito editors",
1168 booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1171 publisher = "Springer-Verlag",
1176 author = "Peter Aczel",
1177 title = "On Relating Type Theories and Set Theories",
1178 journal = "Lecture Notes in Computer Science",
1183 @inproceedings{remathematization,
1184 author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1185 title = "{XML}, Stylesheets and the re-mathematization of Formal Content",
1186 booktitle = "EXTREME",
1191 @phdthesis{YANNTHESIS,
1192 author = "Yann Coscoy",
1193 title = "Explication textuelle de preuves pour le {C}alcul des
1194 {C}onstructions {I}nductives",
1195 school = "Universit\'e de Nice-Sophia Antipolis",
1200 author = "Sylvain Lippi",
1201 title = "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)",
1202 school = "Universit\'e Aix-Marseille 2",
1207 author = "Benjamin Werner",
1208 title = "Une Th\'eorie des {C}onstructions {I}nductives",
1209 school = "Universit\'e Paris VII",
1214 @InCollection{Felleisen87,
1215 author = "M. Felleisen and D. Friedman",
1216 editor = "M. Wirsing",
1217 title = "Control operators, the {SECD}-machine, and the lambda calculus",
1218 booktitle = "Formal Description of Programming Concepts III",
1220 publisher = "Elsevier Science Publishers B.V.",
1221 address = "(North-Holland) Amsterdam",
1226 author = "Jan Zwanenburg",
1227 institution = "Eindhoven University of Technology",
1228 number = "Computing Science Report CS-98-11",
1229 title = "The Proof-assistant Yarrow",
1233 @TechReport{Ager2003a,
1234 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1235 institution = "BRICS",
1237 number = "BRICS RS-03-13",
1238 title = "A Functional Correspondence between Evaluators and Abstract Machines",
1242 @TechReport{Ager2003b,
1243 author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1244 institution = "BRICS",
1246 number = "BRICS RS-03-14",
1247 title = "From Interpreter to Compiler and Virtual Machine: A Functional Derivation",
1251 @article{harperpollack,
1252 author = "Robert Harper and Robert Pollack",
1253 title = "Type checking with universes",
1254 journal = "Theoretical Computer Science",
1260 @article{activemath,
1261 author = "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich",
1262 title = "Knowledge Representation and Management in {ActiveMath}",
1263 journal = "Annals of Mathematics and Artificial Intelligence",
1271 author = "Andrea Asperti and Ferruccio Guidi and Luca Padovani and
1272 Claudio Sacerdoti Coen and Irene Schena",
1273 title = "Mathematical Knowledge Management in {HELM}",
1274 journal = "Annals of Mathematics and Artificial Intelligence",
1281 @unpublished{formal-topology,
1282 author = "Giovanni Sambin",
1283 title = "Some points in formal topology",
1284 note = "To appear in Theoretical Computer Science",
1288 @TechReport{JohnHarrison:complexity-of-floating-point-proofs,
1289 author = "John Harrison",
1290 title = "Real Numbers in Real Applications",
1291 note = "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002",
1292 institution = "NASA",
1293 number = "NASA/CP-2002-211736",
1297 @inproceedings{kohlhase-anghelache,
1298 author = "Michael Kohlhase and Romeo Anghelache",
1299 title = "Towards Collaborative Content Management And Version Control For
1300 Structured Mathematical Knowledge",
1301 editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
1302 booktitle = "Proceedings of the Second International Conference on
1303 Mathematical Knowledge Management, MKM 2003",
1305 volume = "LNCS, 2594",
1306 publisher = "Springer-Verlag",
1310 %%% Unused entries from my Master dissertation bibliography
1313 title="{Standard Generalized Markup Language (SGML)}",
1314 note="ISO 8879:1986",
1319 author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1320 title = "{Content Centric Logical Environments}",
1321 note = "Short Presentation at LICS 2000",
1322 ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz",
1326 author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1327 title = "{Formal Mathematics in MathML}",
1328 note = "To be presented at MathML International Conference 2000",
1332 author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1333 title = "{Towards a Library of Formal Mathematics}",
1334 note = "Accepted at TPHOLS 2000",
1335 ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz",
1338 @techreport{mowgli:D4a,
1339 author = "Hanane Naciri and Luca Padovani",
1340 title = "{MathML} Rendering/Browsing Engine",
1341 type = {MoWGLI Report},
1344 howpublished = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}"
1347 @techreport{hazewinkel,
1348 author = "Michiel Hazewinkel",
1349 title = "Dynamic stochastic models for indexes and thesauri,
1350 identification clouds, and information retrieval and
1352 type = "{MKM Net Report}",
1353 howpublished = "\url{http://monet.nag.co.uk/mkm//index.html}"
1356 @techreport{BarrasB:coqpar,
1357 author = "{Barras B.} and {Boutin S.} and {Cornes C.}
1358 and {Courant J.} and {Filliatre J. C.}
1359 and {Gim\'enez E.} and {Herbelin H.} and {Huet G.}
1360 and {Munoz C.} and {Murthy C.} and {Parent C.}
1361 and {Paulin-Mohring C.} and {Saibi A.}
1363 title = "{The Coq Proof Assistant Reference Manual : Version
1365 institution = {Inria (Institut National de Recherche en Informatique
1366 et en Automatique), France},
1367 type = {Technical Report},
1370 author_acronym = {WernerB},
1371 bibdate = {May 1, 1997},
1372 source = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/},
1373 source-date = {Mon 11 Sep 100},
1374 title_acronym = {coqpar}
1377 @unpublished{bw:1997,
1378 author = "Bruno Barras and Benjamin Werner",
1379 title = "{Coq in Coq}",
1382 ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz",
1385 @unpublished{berners-lee:1989,
1386 author = "Tim Berners-Lee",
1387 title = "{Information Management: A Proposal}",
1389 ps = "http://www.w3.org/History/1989/proposal.html",
1392 @techreport{natural,
1393 author = "Yann Coscoy and Gilles Kahn and Laurent Thery",
1394 title = "{Extracting Text from Proofs}",
1395 institution = {Inria (Institut National de Recherche en Informatique
1396 et en Automatique), France},
1397 type = {Technical Report},
1402 @inproceedings{Bru80,
1403 author = "de Bruijn, N. G.",
1404 title = "{A survey of the project AUTOMATH}",
1406 editor = "J. P. Seldin and J. R. Hindley",
1407 booktitle = "To H. B. Curry: Essays in Combinatory Logic,
1408 Lambda Calculus and Formalism",
1410 publisher = "Academic Press"
1413 @techreport{tutrect,
1414 author = "E Gim\'enez",
1415 title = "{A Tutorial on Recursive Types in Coq}",
1416 institution = {Inria (Institut National de Recherche en Informatique
1417 et en Automatique), France},
1418 type = {Technical Report},
1424 author = "John Harrison",
1425 title = "{The QED Manifesto}",
1427 booktitle = "Automated Deduction - CADE 12",
1428 series = "Lecture Notes in Artificial Intelligence",
1431 publisher = "Springer-Verlag"
1434 @inproceedings{harrison-mizar,
1435 author = "John Harrison",
1436 title = "{A Mizar Mode for HOL}",
1438 editor = "Joakim von Wright and Jim Grundy and John Harrison",
1439 booktitle = "Theorem Proving in Higher Order Logics:
1440 9th International Conference, TPHOLs'96",
1441 series = "Lecture Notes in Computer Science",
1443 address = "Turku, Finland",
1444 date = "26--30 August 1996",
1446 publisher = "Springer-Verlag"
1449 @inproceedings{proverb,
1450 author="H. Horacek",
1451 title="{Presenting Proofs in a Human Oriented Way}",
1452 booktitle="16th International Conference on Automated Deduction",
1457 author = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring",
1458 title = "{The Coq Proof Assistant. A Tutorial}",
1463 author="{Jutting van L. S. B.}",
1464 school = {{Eindhoven University of Technology}},
1465 title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}",
1466 type = {Ph D. thesis},
1467 note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}",
1471 @misc{abriefhistoryoftheinternet,
1472 author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.}
1473 and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.}
1474 and {Postel J.} and {Roberts L. G.} and {Wolff S.}",
1475 title="{A Brief Hystory of the Internet}",
1476 note="http://www.isoc.org/internet-history/brief.html"
1479 @inproceedings{MacKenzie:1995,
1480 author="{MacKenzie D.}",
1481 title="{The automation of proof: A historical and sociological exploration}",
1482 booktitle="IEEE: Annals of the History of Computing",
1487 author = "Christine Paulin-Mohring",
1489 school = {{Paris 7}},
1490 title = "{Extraction de programmes dans le Calcul des Constructions}",
1491 type = {Th\`ese d'universit\'e},
1493 url = {http://www.lri.fr/~paulin/these.ps.gz},
1497 author = "A. Ricci",
1498 school = {{Universit\`a degli studi di Bologna}},
1499 title = "{Studio e progettazione di un modello RDF per biblioteche matematiche
1501 type = {Tesi universitaria},
1505 @inproceedings{Rob65,
1506 author="{Robinson J. A.}",
1507 title = "{A machine-oriented logic based on the resolution principle}",
1509 booktitle = "Journal of the ACM",
1514 @inproceedings{sh:1995,
1515 author="{Saibi A.} and {Huet G.}",
1516 title="{Constructive Category Theory}",
1517 booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory",
1518 address="Goteborg (Sweden)",
1523 @inproceedings{ranta2,
1524 author="Thomas Hallgren and Aarne Ranta",
1525 title="An extensible proof text editor",
1526 BOOKTITLE = {LPAR'2000},
1527 SERIES = {LNCS/LNAI},
1532 @inproceedings{werner:1997,
1533 author="Benjamin Werner",
1534 title="{Constructive Category Theory}",
1535 booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software",