helm/papers/matita/matita.bib

   1
   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},
   6  year = {2003},
   7  isbn = {3-540-00568-4},
   8  pages = {66--79},
   9  publisher = {Springer-Verlag},
  10  address = {London, UK},
  11 }
  12
  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",
  18   series = "LNCS",
  19   volume = "3286",
  20   pages = "469--487",
  21   publisher = "Springer-Verlag",
  22   year = 2004,
  23 }
  24
  25 @techreport{mmode,
  26   author = "Freek Wiedijk",
  27   title = "MMode, a Mizar Mode for the proof assistant Coq",
  28   institution = "University of Nijmegen",
  29   number = "NIII-R0333",
  30   year = "2003"
  31 }
  32
  33 @article{ lamport-proof,
  34     author = "Leslie Lamport",
  35     title = "How to write a proof",
  36     journal = "American Mathematical Monthly",
  37     volume = "102",
  38     number = "7",
  39     pages = "600--608",
  40     year = "1995",
  41 }
  42
  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",
  48   year = 2003
  49 }
  50
  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",
  55   series = "LNCS",
  56   volume = "3130,",
  57   pages = "125--138",
  58   year = 2004,
  59   publisher = "Springer-Verlag",
  60 }
  61
  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)",
  66   year = 1996
  67 }
  68
  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",
  74   volume = "789",
  75   year = 1993
  76 }
  77
  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",
  83   year = 2003
  84 }
  85
  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",
  90   year = 1995
  91 }
  92
  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",
  98   year = 1996
  99 }
 100
 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},
 107   YEAR = 2005
 108 }
 109
 110 @article{fourcolor,
 111   author =  "K. Appel and W. Haken",
 112   title =  "Every planar map is four colorable.",
 113   journal =  {Illinois Journal of Mathematics},
 114   year =   1977,
 115   volume =   {21},
 116   pages =    {429--567}
 117 }
 118
 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}"
 123 }
 124
 125 @misc{zmath,
 126         title =  "Zentralblatt MATH",
 127         howpublished = "\url{http://www.emis.de/ZMATH/}"
 128 }
 129
 130 @inproceedings{lcf,
 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},
 134   volume = 78,
 135   publisher = {{Sprin\-ger-Verlag}},
 136   year = 1979
 137 }
 138
 139 @phdthesis{csc-phd,
 140         author = "Claudio {Sacerdoti Coen}",
 141         title = "Mathematical Knowledge Management and Interactive Theorem
 142                 Proving",
 143         school = "University of Bologna",
 144         year = "2004",
 145         note = "Technical Report UBLCS 2004-5"
 146 }
 147
 148 @inproceedings{Isar,
 149   author = "Markus Wenzel",
 150   title = "Isar - A Generic Interpretative Approach to Readable Formal Proof Documents",
 151   booktitle = "Theorem Proving in Higher Order Logics",
 152   pages = "167-184",
 153   year = "1999"
 154 }
 155
 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",
 161   volume = "24",
 162   number = "2",
 163   publisher = "ACM Press",
 164   address = "New York, NY",
 165   pages = "14--24",
 166   year = "1989",
 167   url = "citeseer.nj.nec.com/borras88centaur.html"
 168 }
 169
 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},
 174   YEAR = 1994,
 175   PUBLISHER = {ACM Press},
 176   PAGES = {109--122},
 177   URL = {http://pauillac.inria.fr/~xleroy/publi/manifest-types-popl.ps.gz}
 178 }
 179
 180 @inproceedings{overkilling,
 181   author    = "Claudio {Sacerdoti Coen}",
 182   title     = "Tactics in Modern Proof-Assistants: the Bad Habit of
 183                Overkilling",
 184   booktitle = "Supplementary Proceedings of the 14th International
 185                Conference TPHOLS 2001",
 186   pages     =  {352--367},
 187   year      =  2001
 188 }
 189
 190 @inproceedings{omegaants1,
 191   author =   "Christoph Benzm{\"u}ller and Volker Sorge",
 192   title =  {{OANTS} -- An open approach at combining Interactive and Automated
 193             Theorem Proving},
 194   booktitle =  {Symbolic Computation and Automated Reasoning},
 195   editor =       {Manfred Kerber and Michael Kohlhase},
 196   year =   2000,
 197   pages =        {81--97},
 198   publisher =  {A.K.Peters},
 199   url =    {www.ags.uni-sb.de/~chris/papers/C8.pdf}
 200 }
 201
 202 @article{ocr,
 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},
 206   year =   1996,
 207   volume =   {7},
 208   pages =    {2--15},
 209   number =   {1},
 210   month = mar,
 211   url =    {www.ags.uni-sb.de/~chris/papers/J4.pdf}
 212 }
 213
 214 @article{newauthomath,
 215   author =  "Freek Wiedijk",
 216   title =  "A new implementation of {A}utomath",
 217   journal =  {Journal of Automated Reasoning},
 218   year =   2002,
 219   volume =   {29},
 220   pages =    {365--387}
 221 }
 222
 223 @article{gdome2,
 224   author =  "Paolo Casarini and Luca Padovani",
 225   title =  "The {G}nome {DOM} {E}ngine",
 226   journal =  "Markup Languages: Theory \& Practice",
 227   year =   2002,
 228   volume =   {3},
 229   pages =    {173--190},
 230   number =   {2},
 231   publisher = "MIT Press",
 232   month = apr
 233 }
 234
 235 @article{omegaants2,
 236   author =  "Christoph Benzm{\"u}ller and Mateja Jamnik and Manfred Kerber and
 237              Volker Sorge",
 238   title =  {Agent based Mathematical Reasoning},
 239   journal =  {Electronic Notes in Theoretical Computer Science, Elsevier},
 240   year =   1999,
 241   volume =   {23},
 242   pages =        {21--33},
 243   number =   {3},
 244   url =    {www.ags.uni-sb.de/~chris/papers/J4.pdf}
 245 }
 246
 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",
 253   editor = "{USENIX}",
 254   pages = "229--243",
 255   year = "1996",
 256   url = "citeseer.nj.nec.com/necula96safe.html"
 257 }
 258
 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},
 266   VOLUME = 2410,
 267   PAGES = {115--130},
 268   YEAR = 2002,
 269   PUBLISHER = {{Sprin\-ger-Verlag}},
 270   MONTH = AUG,
 271   ADDRESS = {Hampton, VA, USA}
 272 }
 273
 274 @inproceedings{NL98,
 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",
 279         year="1998"
 280 }
 281
 282 @book{GirardJY:prot,
 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},
 287   year            = 1989
 288 }
 289
 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",
 294   series          = "LNCS",
 295   volume          = "1785",
 296   month           = jan,
 297   year            = 2000,
 298   publisher       = "Springer-Verlag",
 299 }
 300
 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",
 305   series          = "LNCS",
 306   volume          = 996,
 307   year            = 1994,
 308   publisher       = "Springer-Verlag",
 309   note            = "Extended version in LIP research report 95-07, ENS Lyon",
 310   pages           = "39--59",
 311 }
 312
 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}",
 319   volume          = 2,
 320   year            = 1992
 321 }
 322
 323 @inproceedings{coquand:1986,
 324   author="Thierry Coquand",
 325   title="{An Analysis of Girard's Paradox}",
 326   booktitle="Symposium on Logic in Computer Science",
 327   address="Cambridge",
 328   publisher="MA. IEEE press",
 329   year="1986"
 330 }
 331
 332 @phdthesis{mohring,
 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},
 336   YEAR = 1996,
 337   MONTH = DEC,
 338   TYPE = {Habilitation \`a diriger les recherches},
 339   URL = {http://www.lri.fr/~paulin/habilitation.ps.gz}
 340 }
 341
 342 @phdthesis{garrigue,
 343   author          = "Jacques Garrigue",
 344   title           = "{Label-Selective Lambda-Calculi and Transformation Calculi}",
 345   school          = "University of Tokyo, Department of Information Science",
 346   month           = mar,
 347   year            = 1995
 348 }
 349
 350 @phdthesis{LuoZ:extcc,
 351   author          = "Zhaohui Luo",
 352   title           = "{An Extended Calculus of Constructions}",
 353   school          = "University of Edinburgh",
 354   year            = 1990
 355 }
 356
 357 @phdthesis{chicly,
 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",
 362   year            = 2003
 363 }
 364
 365 @phdthesis{geuvers:1993,
 366   author="Herman Geuvers",
 367   title="{Logics and Type Systems}",
 368   school="Catholic University Nijmegen",
 369   year="1993",
 370   type="{Ph.D.} dissertation"
 371 }
 372
 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}",
 377   month = aug,
 378   year = 2002
 379 }
 380
 381 @unpublished{danosKAM,
 382   author = "Vincent Danos and Laurent Regnier",
 383   title = "How abstract machines implement head linear reduction",
 384   year = 2003
 385 }
 386
 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}",
 395   year =         "2001"
 396 }
 397
 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",
 404   year =      "2003",
 405 }
 406
 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",
 412   pages =     "25--36",
 413   publisher = "Kluwer",
 414   year =      "2003",
 415 }
 416
 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",
 422   pages =     "240--258",
 423   volume =    "LNCS, 2646",
 424   publisher = "Springer-Verlag",
 425   year =      "2003",
 426 }
 427
 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",
 434   pages =        "332--346",
 435   publisher =    "Springer-Verlag",
 436   year =         "2004"
 437 }
 438
 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",
 445   pages =        "347--362",
 446   publisher =    "Springer-Verlag",
 447   year =         "2004"
 448 }
 449
 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",
 456   pages =        "14--23",
 457   publisher =    "Springer-Verlag",
 458   year =         "2003"
 459 }
 460
 461 @inproceedings{whelp,
 462   author = "Andrea Asperti and Ferruccio Guidi and Claudio {Sacerdoti Coen}
 463             and Enrico Tassi and Stefano Zacchiroli",
 464   title =        "A content based mathematical search engine: Whelp",
 465   booktitle =    "Post-proceedings of the Types 2004 International Conference",
 466   volume =       "LNCS, 3839",
 467   pages =        "17--32",
 468   publisher =    "Springer-Verlag",
 469   year =         "2004"
 470 }
 471
 472 @inproceedings{exportation-module,
 473   author = "Claudio {Sacerdoti Coen}",
 474   title = "From Proof-Assistans to Distributed Libraries of Mathematics: Tips
 475            and Pitfalls",
 476   editor =       "Andrea Asperti and Bruno Buchberger and James H. Davenport",
 477   booktitle =    "Proceedings of the Second International Conference on
 478                   Mathematical Knowledge Management, MKM 2003",
 479   pages =        "30--44",
 480   volume =       "LNCS, 2594",
 481   publisher =    "Springer-Verlag",
 482   year =         "2003",
 483 }
 484
 485 @inproceedings{ida,
 486   author = "Andrea Asperti and Herman Geuvers and Iris Loeb
 487             and Lionel Elie Mamane and Claudio {Sacerdoti Coen}",
 488   title = "An Interactive Algebra Course with Formalised Proofs and Definitions",
 489   editor =       "Andrea Asperti and Bruno Buchberger and James H. Davenport",
 490   booktitle =    "Post-Proceedings of the Fourth International Conference on Mathematical Knowledge Management, MKM 2005",
 491   pages =        "XXX--XXX",
 492   volume =       "LNCS, (to appear)",
 493   publisher =    "Springer-Verlag",
 494   year =         "2005",
 495 }
 496
 497 @inproceedings{davenport,
 498   author = "James H. Davenport",
 499   title = "{MKM} from Book to Computer: A Case Study",
 500   editor =       "Andrea Asperti and Bruno Buchberger and James H. Davenport",
 501   booktitle =    "Proceedings of the Second International Conference on
 502                   Mathematical Knowledge Management, MKM 2003",
 503   pages =        "17--29",
 504   volume =       "LNCS, 2594",
 505   publisher =    "Springer-Verlag",
 506   year =         "2003",
 507 }
 508
 509 @inproceedings{fguidisacerdot,
 510   author = "Ferruccio Guidi and Claudio {Sacerdoti Coen}",
 511   title = "Querying Distributed Digital Libraries of Mathematics",
 512   editor =       "Therese Hardin and Renaud Rioboo",
 513   booktitle =    "Calculemus 2003",
 514   pages =        "17--30",
 515   publisher =    "Aracne Editrice S.R.L.",
 516   year =         "2003",
 517   note = "ISBN 88-7999-545-6"
 518 }
 519
 520 @inproceedings{hbugs,
 521   author = "Claudio {Sacerdoti Coen} and Stefano Zacchiroli",
 522   title = "Brokers and {W}eb-Services for Automatic Deduction: a Case Study",
 523   editor =       "Therese Hardin and Renaud Rioboo",
 524   booktitle =    "Calculemus 2003",
 525   pages =        "43--57",
 526   publisher =    "Aracne Editrice S.R.L.",
 527   year =         "2003",
 528   note = "ISBN 88-7999-545-6"
 529 }
 530
 531 @inproceedings{calculemus-presentation,
 532   author = "Christoph Benzm{\"u}ller",
 533   title = "The {CALCULEMUS} Research Training Network -- A short Overview",
 534   editor =       "Therese Hardin and Renaud Rioboo",
 535   booktitle =    "Calculemus 2003",
 536   pages =        "1--16",
 537   publisher =    "Aracne Editrice S.R.L.",
 538   year =         "2003",
 539   note = "ISBN 88-7999-545-6"
 540 }
 541
 542 @inproceedings{linda,
 543   author = "Claudio {Sacerdoti Coen}",
 544   title = "A Constructive Proof of the Soundness of the
 545      Encoding of Random Access Machines in a Linda Calculus with Ordered
 546      Semantics",
 547   booktitle = "Theoretical Computer Science: 8th Italian Conference, ICTCS 2003",
 548   pages =        "37--57",
 549   volume =       "LNCS, 2841",
 550   publisher =    "Springer-Verlag",
 551   year =         "2003",
 552 }
 553
 554 @article{asperti-categorical-understanding,
 555   author = "Andrea Asperti",
 556   title = "A categorical understanding of environment machines",
 557   journal = "Journal of Functional Programming",
 558   volume = "2",
 559   number = "1",
 560   pages = "23--59",
 561   month = jan,
 562   year = "1992"
 563 }
 564
 565 @article{namelessdummies,
 566   author = "{N. G. de Bruijn}",
 567   title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem",
 568   journal = "Indagationes Mathematicae",
 569   volume = "34",
 570   pages = "381--392",
 571   year = "1972"
 572 }
 573
 574 @article{ctcoq1,
 575   author = "Yves Bertot",
 576   title = "The CtCoq System: Design and Architecture",
 577   journal = "Formal Aspects of Computing",
 578   volume = "11",
 579   pages = "225--243",
 580   year = "1999"
 581 }
 582
 583 @TechReport{ctcoq2,
 584   author =       "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
 585   title =        "Real Theorem Provers Deserve Real User-Interfaces",
 586   month =        may,
 587   year =         "1992",
 588   institution =  "INRIA",
 589   number =       "{Inria Research Report 1684}"
 590 }
 591
 592 @article{ctcoq3,
 593   author = "Yves Bertot and Laurent Th\'ery",
 594   title = "A Generic Approach to Building User Interfaces for Theorem Provers",
 595   journal = "Journal of Symbolic Computation",
 596   volume = "25",
 597   pages = "161--194",
 598   year = "1998"
 599 }
 600
 601 @article{mbase,
 602   author = "Michael Kohlhase and Andreas Franke",
 603   title = "{MBase}: Representing Knowledge and Context for the Integration of Mathematical Software Systems",
 604   journal = "Journal of Symbolic Computation",
 605   volume = "32",
 606   number = "4",
 607   pages = "365--402",
 608   year = "2001",
 609   url = "\url{http://citeseer.nj.nec.com/kohlhase00mbase.html}"
 610 }
 611
 612 @inproceedings{mizarql,
 613   author = "Grzegorz Bancerek and Piotr Rudnicki",
 614   title = "Information Retrieval in {MML}",
 615   editor =       "Andrea Asperti and Bruno Buchberger and James H. Davenport",
 616   booktitle =    "Proceedings of the Second International Conference on
 617                   Mathematical Knowledge Management, MKM 2003",
 618   pages =        "119--132",
 619   volume =       "LNCS, 2594",
 620   publisher =    "Springer-Verlag",
 621   year =         "2003",
 622 }
 623
 624 @article{codedcontexttrees,
 625   author = "Harald Ganzinger and Robert Nieuwehuis and Pilar Nivela",
 626   title = "Fast Term Indexing with Coded Context Trees. Journal of Automated Reasoning",
 627   journal = "Journal of Automated Reasoning",
 628   year = "To appear"
 629 }
 630
 631 @article{ranta,
 632   author = "Aarne Ranta",
 633   title = "Grammatical Framework: A Type-Theoretical Grammar Formalism",
 634   journal = "Journal of Functional Programming",
 635   year = "To appear",
 636   note = "Manuscript made available in September 2002"
 637 }
 638
 639 @book{DiCosmo,
 640   AUTHOR = "Di Cosmo, Roberto",
 641   TITLE = {Isomorphisms of types: from $\lambda$-calculus to  information retrieval and language design},
 642   SERIES = {Progress in Theoretical Computer Science},
 643   PUBLISHER = {Birkhauser},
 644   YEAR = {1995},
 645   NOTE = {ISBN-0-8176-3763-X}
 646 }
 647
 648 @book{automath,
 649   EDITOR = "R.P. Nederpelt and J.H. Geuvers and R.C. de Vrijer",
 650   TITLE = {Selected Papers on Automath},
 651   SERIES = {Studies in Logic and the Foundations of Mathematics},
 652   PUBLISHER = {Elsevier Science},
 653   VOLUME = "133",
 654   YEAR = {1994},
 655   NOTE = {ISBN-0444898220}
 656 }
 657
 658 @misc{krivine,
 659  author = "Jean-Louis Krivine",
 660  title = "Un interpr\`ete du $\lambda$-calcul",
 661  howpublished = "Brouillon. Available on-line at \url{http://www.logique.jussieu.fr/~krivine}",
 662  year = 1985
 663 }
 664
 665 @misc{na-mkm1,
 666  title = "Progress Report: Building Interactive Digital Libraries of Formal
 667           Algorithmic Knowledge",
 668  howpublished = "Cornell University, \url{http://www.cs.uwyo.edu/~nuprl/documents/cornell_slides.pdf}",
 669  month = may,
 670  year = 2002,
 671  key = "Progress"
 672 }
 673
 674 @misc{metadata4education,
 675  title = "{L}earning {O}bject {M}etadata Standard",
 676  howpublished = "Learning Technology Standards Committee of IEEE, \verb+http://www.learninglab.de/elan/kb3/lexikon/metadaten-standards/docs/+ \verb+LOM_1484_12_1_v1_Final_Draft.pdf+",
 677  year = 2002,
 678  key = "Learning"
 679 }
 680
 681 @misc{openmath-cd-with-plus,
 682  title = "Arith1 {OpenMath} {C}ontent {D}ictionary",
 683  howpublished = "The OpenMath Society, \url{http://www.openmath.org/cocoon/openmath/cd/arith1.ocd}",
 684  year = 2002,
 685  key = "Arith1 OpenMath Content Dictionary"
 686 }
 687
 688
 689 @misc{ddc,
 690  title = "Dewey Decimal Classification",
 691  howpublished = "\url{http://www.oclc.org/dewey}",
 692  url = "\url{http://www.oclc.org/dewey}",
 693  key = "Dewey"
 694 }
 695
 696 @misc{lc,
 697  title = "Library of Congress Classification Scheme",
 698  howpublished = "\url{http://www.loc.gov}",
 699  url = "\url{http://www.loc.gov}",
 700  key = "Library"
 701 }
 702
 703 @misc{msc,
 704  title = "Mathematical {S}ubject {C}lassification, {A}merican {M}athematical {S}ociety",
 705  howpublished = "\url{http://www.ams.org/msc}",
 706  url = "\url{http://www.ams.org/msc}",
 707  key = "Mathematical"
 708 }
 709
 710 @InCollection{borges,
 711  author = "Jorge Luis Borges",
 712  title = "The Library of {B}abel",
 713  publisher = "Grove Press",
 714  booktitle = "Ficciones",
 715  year = 1942
 716 }
 717
 718 @inproceedings{magaud,
 719  author = "Nicolas Magaud",
 720  title = "{C}hanging {D}ata {R}epresentation within the {C}oq {S}ystem",
 721  booktitle = {TPHOLs'2003},
 722  publisher = {Springer-Verlag},
 723  volume = {LNCS, 2758},
 724  year = {2003},
 725 }
 726
 727 @inproceedings{geuvers-jojgov,
 728   author =       "Herman Geuvers and Gueorgui I. Jojgov",
 729   title =        "Open Proofs and Open Terms: A Basis for Interactive Logic",
 730   editor =       "J. Bradfield",
 731   booktitle =    "Computer Science Logic: 16th International Workshop, CLS 2002",
 732   pages =        "537-552",
 733   volume =       "LNCS, 2471",
 734   publisher =    "Springer-Verlag",
 735   month =        jan,
 736   year =         "2002"
 737 }
 738
 739 @inproceedings{mkm-structure,
 740   author =       "Koji Nakagawa and Akihiro Nomura and Masakazu Suzuki",
 741   title =        "Extraction of Logical Structure from articles in Mathematics",
 742   editor =       "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
 743   booktitle =    "Proceedings of Mathematical Knowledge Management 2004",
 744   volume =       "LNCS, 3119",
 745   pages =        "276--289",
 746   publisher =    "Springer-Verlag",
 747   year =         "2004"
 748 }
 749
 750 @inproceedings{mkm-metadata2,
 751   author =       "Andrea Asperti and Matteo Selmi",
 752   title =        "Efficient Retrieval of Mathematical Statements",
 753   editor =       "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
 754   booktitle =    "Proceedings of Mathematical Knowledge Management 2004",
 755   volume =       "LNCS, 3119",
 756   pages =        "17--31",
 757   publisher =    "Springer-Verlag",
 758   year =         "2004"
 759 }
 760
 761 @inproceedings{adams,
 762   author =       "A. A. Adams",
 763   title =        "Digitisation, Representation and Formalisation: Digital
 764                   Libraries of Mathematics.",
 765   editor =       "A. Asperti, B. Buchberger, J.H. Davenport",
 766   booktitle =    "Proceedings of Mathematical Knowledge Management 2003",
 767   volume =       "LNCS, 2594",
 768   pages =        "1--16",
 769   publisher =    "Springer-Verlag",
 770   year =         "2003"
 771 }
 772
 773 @inproceedings{maya,
 774   author =       "Serge Autexier and Dieter Hutter and Heiko Mantel and Axel Schairer",
 775   title =        "Towards an Evolutionary Formal Software-Development Using {CASL}",
 776   booktitle =    "WADT99 Selected Papers Volume",
 777   volume =       "LNCS, 1827",
 778   publisher =    "Springer-Verlag",
 779   year =         "2000"
 780 }
 781
 782 @inproceedings{how-to-extract,
 783   author =       "Lu\'is Cruz Filipe and Bas Spitters",
 784   title =        "Program Extraction from large proof developments",
 785   booktitle =    "Proceedings of TPHOLS 2003",
 786   editor =       "D. Basin and B. Wolff",
 787   volume =       "LNCS, 2758",
 788   publisher =    "Springer-Verlag",
 789   year =         "2003"
 790 }
 791
 792 @inproceedings{click-and-prove,
 793   author =       "Jean-Raymond Abrial and Dominique Cansell",
 794   title =        "Click'n {P}rove: Interactive Proofs Within Set Theory",
 795   booktitle =    "Proceedings of TPHOLS 2003",
 796   editor =       "D. Basin and B. Wolff",
 797   volume =       "LNCS, 2758",
 798   publisher =    "Springer-Verlag",
 799   year =         "2003"
 800 }
 801
 802 @inproceedings{delahaye,
 803   author =       "David Delahaye and Roberto di Cosmo",
 804   title =        "Information Retrieval in a {C}oq Proof Library using
 805                   Type Isomorphisms",
 806   booktitle =    "Proceedings of TYPES 99",
 807   volume =       "LNCS",
 808   publisher =    "Springer-Verlag",
 809   year =         "1999"
 810 }
 811
 812 @TechReport{jojgov,
 813   author =       "G. I. Jojgov",
 814   title =        "Systems for open terms: An Overview",
 815   institution =  "Technische Universiteit Eindhoven",
 816   number =       "CSR 01-03",
 817   year =         "2001"
 818 }
 819
 820 @TechReport{garrigue:implicit-arguments,
 821   author =       "Jun P. Furuse and Jacques Garrigue",
 822   title =        " A label-selective lambda-calculus with optional arguments and its compilation method",
 823   institution =  "Research Institute for Mathematical Sciences, Kyoto University",
 824   number =       "RIMS Preprint 1041",
 825   month =        oct,
 826   year =         "1995"
 827 }
 828
 829 @phdthesis{miquel,
 830   author =       "Alexandre Miquel",
 831   title =        "Le {C}alcul des {C}onstructions {I}mplicite: syntaxe et s\'emantique",
 832   school =       "Universit\'e Paris 7",
 833   year =         "2001"
 834 }
 835
 836 @phdthesis{chrzaszcz,
 837   author =       "Jacek Chrz{\c{a}}szcs",
 838   title =        "Modules in Type Theory with Generative Definitions",
 839   school =       "Uniwersytet Warszawski and Universit\'e de Paris Sud",
 840   year =         "2003"
 841 }
 842
 843 @phdthesis{Pons,
 844   author =       "Olivier Pons",
 845   title =        "Conception et r\'ealisation d'outils d'aide au d\'eveloppement de grosse th\'eories dans les syst\`emes de preuves interactifs",
 846   school =       "Conservatoire National des Arts et M\'etiers",
 847   year =         "1999"
 848 }
 849
 850 @phdthesis{blanqui,
 851   author =       "Fr\'ed\'eric Blanqui",
 852   title =        "Type Theory and Rewriting",
 853   school =       "Universit\'e Paris XI",
 854   year =         "2001"
 855 }
 856
 857 @phdthesis{magnusson,
 858   author =       "Lena Magnusson",
 859   title =        "The Implementation of {ALF} -- a Proof Editor based
 860                   on Martin-L{\"o}f Monomorphic Type Theory with Explicit
 861                   Substitutions",
 862   school =       "Chalmers University of Technology / G{\"o}teborg University",
 863   year =         "1995"
 864 }
 865
 866 @phdthesis{McBride,
 867   author =       "Conor McBride",
 868   title =        "Dependently Typed Functional Programs and their Proofs",
 869   school =       "University of Edinburgh",
 870   year =         "1999"
 871 }
 872
 873 @phdthesis{schena,
 874   author =       "Irene Schena",
 875   title =        "Towards a Semantic Web for Formal Mathematics",
 876   school =       "University of Bologna",
 877   year =         "2002"
 878 }
 879
 880 @phdthesis{fguidi,
 881   author = "Ferruccio Guidi",
 882   title = "Searching and Retrieving in Content-Based Repositories
 883            of Formal Mathematical Knowledge",
 884   school = "University of Bologna",
 885   month = mar,
 886   year = "2003",
 887   note = "Technical Report UBLCS 2003-06"
 888 }
 889
 890 @phdthesis{padovani,
 891   author = "Luca Padovani",
 892   title = "MathML Formatting",
 893   school = "University of Bologna",
 894   month = feb,
 895   year = "2003",
 896   note = "Technical Report UBLCS 2003-03"
 897 }
 898
 899 @mastersthesis{csc-master,
 900   author = "Claudio {Sacerdoti Coen}",
 901   title =  "Progettazione e realizzazione con tecnologia {XML} di basi distribuite di conoscenza matematica formalizzata",
 902   school = "University of Bologna",
 903   year =   2000
 904 }
 905
 906 @mastersthesis{zack-master,
 907   author =   "Stefano Zacchiroli",
 908   title =    "Web {s}ervices per il supporto alla dimostrazione interattiva",
 909   school =   "University of Bologna",
 910   year =     2003
 911 }
 912
 913 @mastersthesis{dilena,
 914   author =   "Pietro Dilena",
 915   title =    "Generazione automatica di stylesheet per notazione matematica",
 916   school =   "University of Bologna",
 917   year =     2003
 918 }
 919
 920 @phdthesis{munoz,
 921   author =       "C\'esar Munoz",
 922   title =        "A Calculus of Substitutions for Incomplete-Proof
 923                   Representation in Type Theory",
 924   school =       "INRIA",
 925   month =        nov,
 926   year =         "1997"
 927 }
 928
 929 @phdthesis{strecker,
 930   author =       "Martin Strecker",
 931   title =        "Construction and Deduction in Type Theories",
 932   school =       "Universit{\"a}t Ulm",
 933   year =         1998
 934 }
 935
 936 @misc{content-centric,
 937  author = "Andrea Asperti and Luca padovani
 938            and Claudio {Sacerdoti Coen} and irene Schena",
 939  title = "Content-centric Logical Envirnoments",
 940  howpublished = "Short Presentation at the Fifteenth IEEE Symposium on Logic in Computer Science",
 941  month = "June",
 942  year = "2000",
 943  key = "content centric"
 944 }
 945
 946 @misc{mowgli-proposal,
 947  title = "The {MoWGLI Proposal}, {HTML} Version",
 948  howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/project.html}",
 949  key = "MoWGLI Proposal"
 950 }
 951
 952 @misc{debrujinfactor,
 953  title = "The ``de Bruijn factor''",
 954  howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}",
 955  year = {2000},
 956  author = "Freek Wiedijk",
 957 }
 958
 959 @misc{mowgli-deliverables,
 960  title = "{MoWGLI} Project Deliverables",
 961  howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html}",
 962  key = "MoWGLI Deliverables"
 963 }
 964
 965 @misc{ALF,
 966  title = "The {ALF} family of proof-assistants",
 967  howpublished = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
 968  url = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
 969  key = "ALF"
 970 }
 971
 972 @misc{CoqManual,
 973  title = "The {C}oq Proof Assistant Reference Manual",
 974  author = "{The Coq Development Team}",
 975  howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
 976  year = {2005},
 977  key = "CoqManual"
 978 }
 979
 980 @misc{Coq,
 981  title = "The {C}oq proof-assistant",
 982  howpublished = "\\\url{http://coq.inria.fr}",
 983  key = "Coq"
 984 }
 985
 986 @misc{phox,
 987  title = "The {PhoX} proof-assistant",
 988  howpublished = "\\\url{http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html}",
 989  key = "PhoX"
 990 }
 991
 992 @misc{lego,
 993  title = "The {L}ego proof-assistant",
 994  howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}",
 995  url = "\url{http://www.dcs.ed.ac.uk/home/lego/}",
 996  key = "Lego"
 997 }
 998
 999 @misc{ALFA,
1000  title = "The {A}lfa proof editor",
1001  howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
1002  url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
1003  key = "Alfa"
1004 }
1005
1006 @misc{pvs,
1007  title = "The {PVS} Specification and Verification System",
1008  howpublished = "\\\url{http://pvs.csl.sri.com/}",
1009  key = "PVS"
1010 }
1011
1012 @misc{isabelle,
1013  title = "The {Isabelle} proof-assistant",
1014  howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}",
1015  key = "Isabelle"
1016 }
1017
1018 @book{nuprl-book,
1019   author =    "Constable, Robert L. and Stuart F. Allen and H. M. Bromley and
1020                W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and
1021                T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
1022                Scott F. Smith",
1023   title =     "Implementing Mathematics with the {N}uprl Development System",
1024   publisher = "Prentice-Hall",
1025   year =      1986,
1026   address =   "NJ"
1027 }
1028
1029 @misc{nuprl,
1030  title = "The {NuPRL} proof-assistant",
1031  howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
1032  key = "NuPRL"
1033 }
1034
1035 @misc{hollight,
1036  title = "The {HOL Light} proof-assistant",
1037  howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}",
1038  key = "HOL-Light"
1039 }
1040
1041 @misc{monet,
1042  title = "The {MONET} project",
1043  howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}",
1044  key = "Monet"
1045 }
1046
1047 @misc{calculemus,
1048  title = "The {CALCULEMUS} project",
1049  howpublished = "\url{http://www.calculemus.net/}",
1050  url = "\url{http://www.calculemus.net/}",
1051  key = "Calculemus"
1052 }
1053
1054 @misc{mizar,
1055  title = "The {M}izar proof-assistant",
1056  howpublished = "\\\url{http://mizar.uwb.edu.pl/}",
1057  key = "Mizar"
1058 }
1059
1060 @misc{openmath,
1061  howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium",
1062  author = "O. Caprotti and D. P. Carlisle and A. M. Cohen",
1063  title = "{\emph{The {O}pen{M}ath {S}tandard}}"
1064 }
1065
1066 @misc{mathml,
1067  title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
1068  editor="{Patrick Ion} and others",
1069  howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
1070  year = {2003},
1071  url = "\url{http://www.w3.org/TR/MathML2}",
1072  key = "MathML"
1073 }
1074
1075 @misc{xml,
1076  title = "{E}xtensible {M}arkup {L}anguage ({XML}).  {V}ersion 1.0.",
1077 editor="{Tim Bray} and others",
1078  howpublished = "W3C Recommendation 10 February 1998,
1079                  \url{http://www.w3.org/TR/REC-xml}",
1080  url = "\url{http://www.w3.org/TR/REC-xml}",
1081  key = "XML"
1082 }
1083
1084 @misc{dom,
1085  title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0",
1086  howpublished = "W3C Candidate Recommendation 10 May 2000,
1087                  \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1088  url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1089  key = "Document"
1090 }
1091
1092 @misc{URIs,
1093  title = "Universal Resource Identifiers in {WWW}",
1094  howpublished = "RFC 1630, CERN",
1095  month = jun,
1096  year = "1994",
1097  key = "URI"
1098 }
1099
1100 @misc{xpath,
1101  title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0",
1102  howpublished = "W3C Recommendation, 16 November 1999,
1103                  \url{http://www.w3.org/TR/xpath}",
1104  url = "\url{http://www.w3.org/TR/xpath}",
1105  key = "XML"
1106 }
1107
1108 @misc{xslt,
1109  title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0",
1110  howpublished = "W3C Recommendation, 16 November 1999,
1111                  \url{http://www.w3.org/TR/xslt}",
1112  url = "\url{http://www.w3.org/TR/xslt}",
1113  key = "XSLT"
1114 }
1115
1116 @misc{rdf,
1117  title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax
1118           Specification",
1119  howpublished = "W3C Recommendation 22 February 1999,
1120                  \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1121  url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1122  key = "Resource"
1123 }
1124
1125 @misc{omdoc,
1126  title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)",
1127  howpublished = "\\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}",
1128  year = {2005},
1129  key = "OMDoc"
1130 }
1131
1132 @misc{FORMAVIE,
1133  title = "The {F}ormavie project",
1134  howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1135  url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1136  key = "Formavie"
1137 }
1138
1139 @misc{EHELM,
1140  title = "The {HELM} project",
1141  howpublished = "\url{http://helm.cs.unibo.it}",
1142  url = "\url{http://helm.cs.unibo.it}",
1143  key = "HELM"
1144 }
1145
1146 @misc{helm-library,
1147  title = "The {HELM} On-Line Library",
1148  howpublished = "\url{http://helm.cs.unibo.it/library.html}",
1149  url = "\url{http://helm.cs.unibo.it/library.html}",
1150  key = "HELM Library"
1151 }
1152
1153 @misc{MATHWEB,
1154  title = "The {M}ath{W}eb project",
1155  howpublished = "\url{http://www.mathweb.org}",
1156  url = "\url{http://www.mathweb.org}",
1157  key = "MathWeb"
1158 }
1159
1160 @misc{PCOQ,
1161  title = "The {PC}oq project",
1162  howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1163  url = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1164  key = "PCoq"
1165 }
1166
1167 @TechReport{HELM,
1168   author =       "Andrea Asperti and Luca Padovani and Claudio {Sacerdoti Coen}
1169                   and Irene Schena",
1170   title =        "Towards a library of formal mathematics",
1171   year =         "2000",
1172   note =         "Panel session of the 13th {I}nternation {C}onference on
1173                   {T}heorem {P}roving in {H}igher {O}rder {L}ogics
1174                   ({TPHOLS}'2000), Portland, Oregon, USA",
1175 }
1176
1177 @inproceedings{Ring,
1178   author =       "Samuel Boutin",
1179   title =        "Using Reflection to Build Efficient and Certified Decision
1180                   Procedures",
1181   editor =       "Martin Abadi and Takahashi Ito editors",
1182   booktitle =    "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1183   pages =        "515-529",
1184   volume =       "1281",
1185   publisher =    "Springer-Verlag",
1186   year =         "1997",
1187 }
1188
1189 @inproceedings{werner-zfc,
1190   author =       "Benjamin Werner",
1191   title =        "Sets in Types, Types in Sets",
1192   editor =       "Martin Abadi and Takahashi Ito editors",
1193   booktitle =    "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1194   pages =        "530-546",
1195   volume =       "1281",
1196   publisher =    "Springer-Verlag",
1197   year =         "1997",
1198 }
1199
1200 @article{aczel,
1201   author = "Peter Aczel",
1202   title = "On Relating Type Theories and Set Theories",
1203   journal = "Lecture Notes in Computer Science",
1204   volume = "1657",
1205   year = "1999",
1206 }
1207
1208 @inproceedings{remathematization,
1209   author =       "Andrea Asperti and Luca Padovani
1210                  and Claudio {Sacerdoti Coen} and Irene Schena",
1211   title =        "{XML}, Stylesheets and the re-mathematization
1212                  of Formal Content",
1213   booktitle =    "EXTREME",
1214   year = "2001",
1215 }
1216
1217
1218 @phdthesis{YANNTHESIS,
1219   author =       "Yann Coscoy",
1220   title =        "Explication textuelle de preuves pour le {C}alcul des
1221                   {C}onstructions {I}nductives",
1222   school =       "Universit\'e de Nice-Sophia Antipolis",
1223   year =         "2000",
1224 }
1225
1226 @phdthesis{Lippi,
1227   author =  "Sylvain Lippi",
1228   title =   "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)",
1229   school =  "Universit\'e Aix-Marseille 2",
1230   year =    "2002"
1231 }
1232
1233 @phdthesis{Werner,
1234   author =       "Benjamin Werner",
1235   title =        "Une Th\'eorie des {C}onstructions {I}nductives",
1236   school =       "Universit\'e Paris VII",
1237   month =        may,
1238   year =         "1994",
1239 }
1240
1241 @InCollection{Felleisen87,
1242   author =       "M. Felleisen and D. Friedman",
1243   editor =       "M. Wirsing",
1244   title =        "Control operators, the {SECD}-machine, and the lambda calculus",
1245   booktitle =    "Formal Description of Programming Concepts III",
1246   pages =        "193--217",
1247   publisher =    "Elsevier Science Publishers B.V.",
1248   address =      "(North-Holland) Amsterdam",
1249   year =         "1987",
1250 }
1251
1252 @TechReport{yarrow,
1253   author =       "Jan Zwanenburg",
1254   institution =  "Eindhoven University of Technology",
1255   number =       "Computing Science Report CS-98-11",
1256   title =        "The Proof-assistant Yarrow",
1257   year =         "1998"
1258 }
1259
1260 @TechReport{Ager2003a,
1261   author =       "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1262   institution =  "BRICS",
1263   month =        mar,
1264   number =       "BRICS RS-03-13",
1265   title =        "A Functional Correspondence between Evaluators and Abstract Machines",
1266   year =         "2003"
1267 }
1268
1269 @TechReport{Ager2003b,
1270   author =       "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1271   institution =  "BRICS",
1272   month =        mar,
1273   number =       "BRICS RS-03-14",
1274   title =        "From Interpreter to Compiler and Virtual Machine: A Functional Derivation",
1275   year =         "2003"
1276 }
1277
1278 @article{harperpollack,
1279   author =       "Robert Harper and Robert Pollack",
1280   title =        "Type checking with universes",
1281   journal =      "Theoretical Computer Science",
1282   volume =       "89",
1283   pages =        "107--136",
1284   year =         "1991"
1285 }
1286
1287 @article{activemath,
1288   author =       "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich",
1289   title =        "Knowledge Representation and Management in {ActiveMath}",
1290   journal =      "Annals of Mathematics and Artificial Intelligence",
1291   volume =       "38(1-3)",
1292   pages =        "47--64",
1293   month =        may,
1294   year =         "2003"
1295 }
1296
1297 @article{mkm-helm,
1298   author =       "Andrea Asperti and Ferruccio Guidi and Luca Padovani and
1299                   Claudio {Sacerdoti Coen} and Irene Schena",
1300   title =        "Mathematical Knowledge Management in {HELM}",
1301   journal =      "Annals of Mathematics and Artificial Intelligence",
1302   volume =       "38(1-3)",
1303   pages =        "27--46",
1304   month =        may,
1305   year =         "2003"
1306 }
1307
1308 @unpublished{formal-topology,
1309    author = "Giovanni Sambin",
1310    title = "Some points in formal topology",
1311    note = "To appear in Theoretical Computer Science",
1312    year = "2002"
1313 }
1314
1315 @TechReport{JohnHarrison:complexity-of-floating-point-proofs,
1316   author =       "John Harrison",
1317   title =        "Real Numbers in Real Applications",
1318   note =    "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002",
1319   institution =  "NASA",
1320   number =       "NASA/CP-2002-211736",
1321   year =         "2002"
1322 }
1323
1324 @inproceedings{kohlhase-anghelache,
1325   author = "Michael Kohlhase and Romeo Anghelache",
1326   title = "Towards Collaborative Content Management And Version Control For
1327            Structured Mathematical Knowledge",
1328   editor =       "Andrea Asperti and Bruno Buchberger and James H. Davenport",
1329   booktitle =    "Proceedings of the Second International Conference on
1330                   Mathematical Knowledge Management, MKM 2003",
1331   pages =        "147--161",
1332   volume =       "LNCS, 2594",
1333   publisher =    "Springer-Verlag",
1334   year =         "2003",
1335 }
1336
1337 %%% Unused entries from my Master dissertation bibliography
1338
1339 @misc{sgml,
1340         title="{Standard Generalized Markup Language (SGML)}",
1341         note="ISO 8879:1986",
1342         key="ISO"
1343         }
1344
1345 @unpublished{helm1,
1346   author = "Andrea Asperti and Luca Padovani
1347            and Claudio {Sacerdoti Coen} and Irene Schena",
1348   title = "{Content Centric Logical Environments}",
1349   note = "Short Presentation at LICS 2000",
1350   ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz",
1351 }
1352
1353 @unpublished{helm4,
1354   author = "Andrea Asperti and Luca Padovani
1355            and Claudio {Sacerdoti Coen} and Irene Schena",
1356   title = "{Formal Mathematics in MathML}",
1357   note = "To be presented at MathML International Conference 2000",
1358 }
1359
1360 @unpublished{helm2,
1361   author = "Andrea Asperti and Luca Padovani
1362            and Claudio {Sacerdoti Coen} and Irene Schena",
1363   title = "{Towards a Library of Formal Mathematics}",
1364   note = "Accepted at TPHOLS 2000",
1365   ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz",
1366 }
1367
1368 @techreport{mowgli:D4a,
1369     author          = "Hanane Naciri and Luca Padovani",
1370     title           = "{MathML} Rendering/Browsing Engine",
1371     type            = {MoWGLI Report},
1372     number          = {D4a},
1373     year            = 2003,
1374     howpublished    = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}"
1375 }
1376
1377 @techreport{hazewinkel,
1378     author          = "Michiel Hazewinkel",
1379     title           = "Dynamic stochastic models for indexes and thesauri,
1380                        identification clouds, and information retrieval and
1381                        storage",
1382     type            = "{MKM Net Report}",
1383     howpublished    = "\url{http://monet.nag.co.uk/mkm//index.html}"
1384 }
1385
1386 @techreport{BarrasB:coqpar,
1387     author          = "{Barras B.} and {Boutin S.} and {Cornes C.}
1388         and {Courant J.} and {Filliatre J. C.}
1389         and {Gim\'enez E.} and {Herbelin H.} and {Huet G.}
1390         and {Munoz C.} and {Murthy C.} and {Parent C.}
1391         and {Paulin-Mohring C.} and {Saibi A.}
1392         and {Werner B.}",
1393     title           = "{The Coq Proof Assistant Reference Manual : Version
1394         6.1}",
1395     institution     = {Inria (Institut National de Recherche en Informatique
1396         et en Automatique), France},
1397     type            = {Technical Report},
1398     number          = {RT-0203},
1399     year            = 1997,
1400     author_acronym  = {WernerB},
1401     bibdate         = {May 1, 1997},
1402     source          = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/},
1403     source-date     = {Mon 11 Sep 100},
1404     title_acronym   = {coqpar}
1405 }
1406
1407 @unpublished{bw:1997,
1408   author = "Bruno Barras and Benjamin Werner",
1409   title = "{Coq in Coq}",
1410   year = "1997",
1411   note = "Submitted",
1412   ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz",
1413 }
1414
1415 @unpublished{berners-lee:1989,
1416   author = "Tim Berners-Lee",
1417   title = "{Information Management: A Proposal}",
1418   year = "1989",
1419   ps = "http://www.w3.org/History/1989/proposal.html",
1420 }
1421
1422 @techreport{natural,
1423     author          = "Yann Coscoy and Gilles Kahn and Laurent Thery",
1424     title           = "{Extracting Text from Proofs}",
1425     institution     = {Inria (Institut National de Recherche en Informatique
1426         et en Automatique), France},
1427     type            = {Technical Report},
1428     number          = {RR-2459},
1429     year            = 1995
1430 }
1431
1432 @inproceedings{Bru80,
1433         author          = "de Bruijn, N. G.",
1434         title           = "{A survey of the project AUTOMATH}",
1435         pages           = "589--606",
1436         editor          = "J. P. Seldin and J. R. Hindley",
1437         booktitle       = "To H. B. Curry: Essays in Combinatory Logic,
1438                            Lambda Calculus and Formalism",
1439         year            = 1980,
1440         publisher       = "Academic Press"
1441 }
1442
1443 @techreport{tutrect,
1444     author          = "E Gim\'enez",
1445     title           = "{A Tutorial on Recursive Types in Coq}",
1446     institution     = {Inria (Institut National de Recherche en Informatique
1447         et en Automatique), France},
1448     type            = {Technical Report},
1449     number          = {RT-0221},
1450     year            = 1998
1451 }
1452
1453 @inproceedings{QED,
1454         author          = "John Harrison",
1455         title           = "{The QED Manifesto}",
1456         pages           = "238--251",
1457         booktitle       = "Automated Deduction - CADE 12",
1458         series          = "Lecture Notes in Artificial Intelligence",
1459         volume          = 814,
1460         year            = 1994,
1461         publisher       = "Springer-Verlag"
1462 }
1463
1464 @inproceedings{harrison-mizar,
1465         author          = "John Harrison",
1466         title           = "{A Mizar Mode for HOL}",
1467         pages           = "203--220",
1468         editor          = "Joakim von Wright and Jim Grundy and John Harrison",
1469         booktitle       = "Theorem Proving in Higher Order Logics:
1470                            9th International Conference, TPHOLs'96",
1471         series          = "Lecture Notes in Computer Science",
1472         volume          = 1125,
1473         address         = "Turku, Finland",
1474         date            = "26--30 August 1996",
1475         year            = 1996,
1476         publisher       = "Springer-Verlag"
1477 }
1478
1479 @inproceedings{proverb,
1480         author="H. Horacek",
1481         title="{Presenting Proofs in a Human Oriented Way}",
1482         booktitle="16th International Conference on Automated Deduction",
1483         year="1999"
1484         }
1485
1486 @misc{HuetG:coqpat,
1487     author          = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring",
1488     title           = "{The Coq Proof Assistant. A Tutorial}",
1489     year            = 1998
1490 }
1491
1492 @PHDTHESIS{BJ94,
1493   author="{Jutting van L. S. B.}",
1494   school = {{Eindhoven University of Technology}},
1495   title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}",
1496   type = {Ph D. thesis},
1497   note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}",
1498   year = {1994}
1499 }
1500
1501 @misc{abriefhistoryoftheinternet,
1502         author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.}
1503          and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.}
1504          and {Postel J.} and {Roberts L. G.} and {Wolff S.}",
1505         title="{A Brief Hystory of the Internet}",
1506         note="http://www.isoc.org/internet-history/brief.html"
1507         }
1508
1509 @inproceedings{MacKenzie:1995,
1510         author="{MacKenzie D.}",
1511         title="{The automation of proof: A historical and sociological exploration}",
1512         booktitle="IEEE: Annals of the History of Computing",
1513         year="1995"
1514 }
1515
1516 @PHDTHESIS{Moh89b,
1517   author = "Christine Paulin-Mohring",
1518   month = {January},
1519   school = {{Paris 7}},
1520   title = "{Extraction de programmes dans le Calcul des Constructions}",
1521   type = {Th\`ese d'universit\'e},
1522   year = {1989},
1523   url = {http://www.lri.fr/~paulin/these.ps.gz},
1524 }
1525
1526 @MASTERTHESIS{ri99,
1527   author = "A. Ricci",
1528   school = {{Universit\`a degli studi di Bologna}},
1529   title = "{Studio e progettazione di un modello RDF per biblioteche matematiche
1530 elettroniche}",
1531   type = {Tesi universitaria},
1532   year = {1999}
1533 }
1534
1535 @inproceedings{Rob65,
1536         author="{Robinson J. A.}",
1537   title = "{A machine-oriented logic based on the resolution principle}",
1538   pages           = "23--41",
1539   booktitle       = "Journal of the ACM",
1540         volume = "2",
1541         year ="1965"
1542 }
1543
1544 @inproceedings{sh:1995,
1545         author="{Saibi A.} and {Huet G.}",
1546         title="{Constructive Category Theory}",
1547         booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory",
1548         address="Goteborg (Sweden)",
1549         month="January",
1550         year="1995"
1551         }
1552
1553 @inproceedings{ranta2,
1554         author="Thomas Hallgren and Aarne Ranta",
1555         title="An extensible proof text editor",
1556   BOOKTITLE = {LPAR'2000},
1557   SERIES = {LNCS/LNAI},
1558   VOLUME = 1955,
1559   YEAR = 2000
1560         }
1561
1562 @inproceedings{werner:1997,
1563         author="Benjamin Werner",
1564         title="{Constructive Category Theory}",
1565         booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software",
1566         year="1997"
1567         }
1568