helm/papers/matita/matita.bib

   1
   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",
   7   series = "LNCS",
   8   volume = "3286",
   9   pages = "469--487",
  10   publisher = "Springer-Verlag",
  11   year = 2004,
  12 }
  13
  14 @techreport{mmode,
  15   author = "Freek Wiedijk",
  16   title = "MMode, a Mizar Mode for the proof assistant Coq",
  17   institution = "University of Nijmegen",
  18   number = "NIII-R0333",
  19   year = "2003"
  20 }
  21
  22 @article{ lamport-proof,
  23     author = "Leslie Lamport",
  24     title = "How to write a proof",
  25     journal = "American Mathematical Monthly",
  26     volume = "102",
  27     number = "7",
  28     pages = "600--608",
  29     year = "1995",
  30 }
  31
  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",
  37   year = 2003
  38 }
  39
  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",
  44   series = "LNCS",
  45   volume = "3130,",
  46   pages = "125--138",
  47   year = 2004,
  48   publisher = "Springer-Verlag",
  49 }
  50
  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)",
  55   year = 1996
  56 }
  57
  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",
  63   volume = "789",
  64   year = 1993
  65 }
  66
  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",
  72   year = 2003
  73 }
  74
  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",
  79   year = 1995
  80 }
  81
  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",
  87   year = 1996
  88 }
  89
  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},
  96   YEAR = 2005
  97 }
  98
  99 @article{fourcolor,
 100   author =  "K. Appel and W. Haken",
 101   title =  "Every planar map is four colorable.",
 102   journal =  {Illinois Journal of Mathematics},
 103   year =   1977,
 104   volume =   {21},
 105   pages =    {429--567}
 106 }
 107
 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}"
 112 }
 113
 114 @misc{zmath,
 115         title =  "Zentralblatt MATH",
 116         howpublished = "\url{http://www.emis.de/ZMATH/}"
 117 }
 118
 119 @inproceedings{lcf,
 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},
 123   volume = 78,
 124   publisher = {{Sprin\-ger-Verlag}},
 125   year = 1979
 126 }
 127
 128 @phdthesis{csc-phd,
 129         author = "Claudio Sacerdoti Coen",
 130         title = "Mathematical Knowledge Management and Interactive Theorem
 131                 Proving",
 132         school = "University of Bologna",
 133         year = "2004",
 134         note = "Technical Report UBLCS 2004-5"
 135 }
 136
 137 @inproceedings{Isar,
 138   author = "Markus Wenzel",
 139   title = "Isar - A Generic Interpretative Approach to Readable Formal Proof Documents",
 140   booktitle = "Theorem Proving in Higher Order Logics",
 141   pages = "167-184",
 142   year = "1999"
 143 }
 144
 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",
 150   volume = "24",
 151   number = "2",
 152   publisher = "ACM Press",
 153   address = "New York, NY",
 154   pages = "14--24",
 155   year = "1989",
 156   url = "citeseer.nj.nec.com/borras88centaur.html"
 157 }
 158
 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},
 163   YEAR = 1994,
 164   PUBLISHER = {ACM Press},
 165   PAGES = {109--122},
 166   URL = {http://pauillac.inria.fr/~xleroy/publi/manifest-types-popl.ps.gz}
 167 }
 168
 169 @inproceedings{overkilling,
 170   author    = "Sacerdoti Coen, Claudio",
 171   title     = "Tactics in Modern Proof-Assistants: the Bad Habit of
 172                Overkilling",
 173   booktitle = "Supplementary Proceedings of the 14th International
 174                Conference TPHOLS 2001",
 175   pages     =  {352--367},
 176   year      =  2001
 177 }
 178
 179 @inproceedings{omegaants1,
 180   author =   "Christoph Benzm{\"u}ller and Volker Sorge",
 181   title =  {{OANTS} -- An open approach at combining Interactive and Automated
 182             Theorem Proving},
 183   booktitle =  {Symbolic Computation and Automated Reasoning},
 184   editor =       {Manfred Kerber and Michael Kohlhase},
 185   year =   2000,
 186   pages =        {81--97},
 187   publisher =  {A.K.Peters},
 188   url =    {www.ags.uni-sb.de/~chris/papers/C8.pdf}
 189 }
 190
 191 @article{ocr,
 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},
 195   year =   1996,
 196   volume =   {7},
 197   pages =    {2--15},
 198   number =   {1},
 199   month = mar,
 200   url =    {www.ags.uni-sb.de/~chris/papers/J4.pdf}
 201 }
 202
 203 @article{newauthomath,
 204   author =  "Freek Wiedijk",
 205   title =  "A new implementation of {A}utomath",
 206   journal =  {Journal of Automated Reasoning},
 207   year =   2002,
 208   volume =   {29},
 209   pages =    {365--387}
 210 }
 211
 212 @article{gdome2,
 213   author =  "Paolo Casarini and Luca Padovani",
 214   title =  "The {G}nome {DOM} {E}ngine",
 215   journal =  "Markup Languages: Theory \& Practice",
 216   year =   2002,
 217   volume =   {3},
 218   pages =    {173--190},
 219   number =   {2},
 220   publisher = "MIT Press",
 221   month = apr
 222 }
 223
 224 @article{omegaants2,
 225   author =  "Christoph Benzm{\"u}ller and Mateja Jamnik and Manfred Kerber and
 226              Volker Sorge",
 227   title =  {Agent based Mathematical Reasoning},
 228   journal =  {Electronic Notes in Theoretical Computer Science, Elsevier},
 229   year =   1999,
 230   volume =   {23},
 231   pages =        {21--33},
 232   number =   {3},
 233   url =    {www.ags.uni-sb.de/~chris/papers/J4.pdf}
 234 }
 235
 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",
 242   editor = "{USENIX}",
 243   pages = "229--243",
 244   year = "1996",
 245   url = "citeseer.nj.nec.com/necula96safe.html"
 246 }
 247
 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},
 255   VOLUME = 2410,
 256   PAGES = {115--130},
 257   YEAR = 2002,
 258   PUBLISHER = {{Sprin\-ger-Verlag}},
 259   MONTH = AUG,
 260   ADDRESS = {Hampton, VA, USA}
 261 }
 262
 263 @inproceedings{NL98,
 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",
 268         year="1998"
 269 }
 270
 271 @book{GirardJY:prot,
 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},
 276   year            = 1989
 277 }
 278
 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",
 283   series          = "LNCS",
 284   volume          = "1785",
 285   month           = jan,
 286   year            = 2000,
 287   publisher       = "Springer-Verlag",
 288 }
 289
 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",
 294   series          = "LNCS",
 295   volume          = 996,
 296   year            = 1994,
 297   publisher       = "Springer-Verlag",
 298   note            = "Extended version in LIP research report 95-07, ENS Lyon",
 299   pages           = "39--59",
 300 }
 301
 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}",
 308   volume          = 2,
 309   year            = 1992
 310 }
 311
 312 @inproceedings{coquand:1986,
 313   author="Thierry Coquand",
 314   title="{An Analysis of Girard's Paradox}",
 315   booktitle="Symposium on Logic in Computer Science",
 316   address="Cambridge",
 317   publisher="MA. IEEE press",
 318   year="1986"
 319 }
 320
 321 @phdthesis{mohring,
 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},
 325   YEAR = 1996,
 326   MONTH = DEC,
 327   TYPE = {Habilitation \`a diriger les recherches},
 328   URL = {http://www.lri.fr/~paulin/habilitation.ps.gz}
 329 }
 330
 331 @phdthesis{garrigue,
 332   author          = "Jacques Garrigue",
 333   title           = "{Label-Selective Lambda-Calculi and Transformation Calculi}",
 334   school          = "University of Tokyo, Department of Information Science",
 335   month           = mar,
 336   year            = 1995
 337 }
 338
 339 @phdthesis{LuoZ:extcc,
 340   author          = "Zhaohui Luo",
 341   title           = "{An Extended Calculus of Constructions}",
 342   school          = "University of Edinburgh",
 343   year            = 1990
 344 }
 345
 346 @phdthesis{chicly,
 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",
 351   year            = 2003
 352 }
 353
 354 @phdthesis{geuvers:1993,
 355   author="Herman Geuvers",
 356   title="{Logics and Type Systems}",
 357   school="Catholic University Nijmegen",
 358   year="1993",
 359   type="{Ph.D.} dissertation"
 360 }
 361
 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}",
 366   month = aug,
 367   year = 2002
 368 }
 369
 370 @unpublished{danosKAM,
 371   author = "Vincent Danos and Laurent Regnier",
 372   title = "How abstract machines implement head linear reduction",
 373   year = 2003
 374 }
 375
 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}",
 384   year =         "2001"
 385 }
 386
 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",
 393   year =      "2003",
 394 }
 395
 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",
 401   pages =     "25--36",
 402   publisher = "Kluwer",
 403   year =      "2003",
 404 }
 405
 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",
 411   pages =     "240--258",
 412   volume =    "LNCS, 2646",
 413   publisher = "Springer-Verlag",
 414   year =      "2003",
 415 }
 416
 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",
 423   pages =        "332--346",
 424   publisher =    "Springer-Verlag",
 425   year =         "2004"
 426 }
 427
 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",
 434   pages =        "347--362",
 435   publisher =    "Springer-Verlag",
 436   year =         "2004"
 437 }
 438
 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",
 445   pages =        "14--23",
 446   publisher =    "Springer-Verlag",
 447   year =         "2003"
 448 }
 449
 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)",
 455   pages =        "xxx--xxx",
 456   publisher =    "Springer-Verlag",
 457   year =         "2004"
 458 }
 459
 460 @inproceedings{exportation-module,
 461   author = "Sacerdoti Coen, Claudio",
 462   title = "From Proof-Assistans to Distributed Libraries of Mathematics: Tips
 463            and Pitfalls",
 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",
 467   pages =        "30--44",
 468   volume =       "LNCS, 2594",
 469   publisher =    "Springer-Verlag",
 470   year =         "2003",
 471 }
 472
 473 @inproceedings{ida,
 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",
 478   pages =        "XXX--XXX",
 479   volume =       "LNCS, (to appear)",
 480   publisher =    "Springer-Verlag",
 481   year =         "2005",
 482 }
 483
 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",
 490   pages =        "17--29",
 491   volume =       "LNCS, 2594",
 492   publisher =    "Springer-Verlag",
 493   year =         "2003",
 494 }
 495
 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",
 501   pages =        "17--30",
 502   publisher =    "Aracne Editrice S.R.L.",
 503   year =         "2003",
 504   note = "ISBN 88-7999-545-6"
 505 }
 506
 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",
 512   pages =        "43--57",
 513   publisher =    "Aracne Editrice S.R.L.",
 514   year =         "2003",
 515   note = "ISBN 88-7999-545-6"
 516 }
 517
 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",
 523   pages =        "1--16",
 524   publisher =    "Aracne Editrice S.R.L.",
 525   year =         "2003",
 526   note = "ISBN 88-7999-545-6"
 527 }
 528
 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
 533      Semantics",
 534   booktitle = "Theoretical Computer Science: 8th Italian Conference, ICTCS 2003",
 535   pages =        "37--57",
 536   volume =       "LNCS, 2841",
 537   publisher =    "Springer-Verlag",
 538   year =         "2003",
 539 }
 540
 541
 542 @article{asperti-categorical-understanding,
 543   author = "Andrea Asperti",
 544   title = "A categorical understanding of environment machines",
 545   journal = "Journal of Functional Programming",
 546   volume = "2",
 547   number = "1",
 548   pages = "23--59",
 549   month = jan,
 550   year = "1992"
 551 }
 552
 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",
 557   volume = "34",
 558   pages = "381--392",
 559   year = "1972"
 560 }
 561
 562 @article{ctcoq1,
 563   author = "Yves Bertot",
 564   title = "The CtCoq System: Design and Architecture",
 565   journal = "Formal Aspects of Computing",
 566   volume = "11",
 567   pages = "225--243",
 568   year = "1999"
 569 }
 570
 571 @article{ctcoq3,
 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",
 575   volume = "25",
 576   pages = "161--194",
 577   year = "1998"
 578 }
 579
 580 @article{mbase,
 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",
 584   volume = "32",
 585   number = "4",
 586   pages = "365--402",
 587   year = "2001",
 588   url = "\url{http://citeseer.nj.nec.com/kohlhase00mbase.html}"
 589 }
 590
 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",
 597   pages =        "119--132",
 598   volume =       "LNCS, 2594",
 599   publisher =    "Springer-Verlag",
 600   year =         "2003",
 601 }
 602
 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",
 607   year = "To appear"
 608 }
 609
 610 @article{ranta,
 611   author = "Aarne Ranta",
 612   title = "Grammatical Framework: A Type-Theoretical Grammar Formalism",
 613   journal = "Journal of Functional Programming",
 614   year = "To appear",
 615   note = "Manuscript made available in September 2002"
 616 }
 617
 618 @book{DiCosmo,
 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},
 623   YEAR = {1995},
 624   NOTE = {ISBN-0-8176-3763-X}
 625 }
 626
 627 @book{automath,
 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},
 632   VOLUME = "133",
 633   YEAR = {1994},
 634   NOTE = {ISBN-0444898220}
 635 }
 636
 637 @misc{krivine,
 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}",
 641  year = 1985
 642 }
 643
 644 @misc{na-mkm1,
 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}",
 648  month = may,
 649  year = 2002,
 650  key = "Progress"
 651 }
 652
 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+",
 656  year = 2002,
 657  key = "Learning"
 658 }
 659
 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}",
 663  year = 2002,
 664  key = "Arith1 OpenMath Content Dictionary"
 665 }
 666
 667
 668 @misc{ddc,
 669  title = "Dewey Decimal Classification",
 670  howpublished = "\url{http://www.oclc.org/dewey}",
 671  url = "\url{http://www.oclc.org/dewey}",
 672  key = "Dewey"
 673 }
 674
 675 @misc{lc,
 676  title = "Library of Congress Classification Scheme",
 677  howpublished = "\url{http://www.loc.gov}",
 678  url = "\url{http://www.loc.gov}",
 679  key = "Library"
 680 }
 681
 682 @misc{msc,
 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}",
 686  key = "Mathematical"
 687 }
 688
 689 @InCollection{borges,
 690  author = "Jorge Luis Borges",
 691  title = "The Library of {B}abel",
 692  publisher = "Grove Press",
 693  booktitle = "Ficciones",
 694  year = 1942
 695 }
 696
 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},
 703  year = {2003},
 704 }
 705
 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",
 711   pages =        "537-552",
 712   volume =       "LNCS, 2471",
 713   publisher =    "Springer-Verlag",
 714   month =        jan,
 715   year =         "2002"
 716 }
 717
 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",
 724   pages =        "276--289",
 725   publisher =    "Springer-Verlag",
 726   year =         "2004"
 727 }
 728
 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",
 735   pages =        "17--31",
 736   publisher =    "Springer-Verlag",
 737   year =         "2004"
 738 }
 739
 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",
 747   pages =        "1--16",
 748   publisher =    "Springer-Verlag",
 749   year =         "2003"
 750 }
 751
 752 @inproceedings{maya,
 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",
 758   year =         "2000"
 759 }
 760
 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",
 768   year =         "2003"
 769 }
 770
 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",
 778   year =         "2003"
 779 }
 780
 781 @inproceedings{delahaye,
 782   author =       "David Delahaye and Roberto di Cosmo",
 783   title =        "Information Retrieval in a {C}oq Proof Library using
 784                   Type Isomorphisms",
 785   booktitle =    "Proceedings of TYPES 99",
 786   volume =       "LNCS",
 787   publisher =    "Springer-Verlag",
 788   year =         "1999"
 789 }
 790
 791 @TechReport{jojgov,
 792   author =       "G. I. Jojgov",
 793   title =        "Systems for open terms: An Overview",
 794   institution =  "Technische Universiteit Eindhoven",
 795   number =       "CSR 01-03",
 796   year =         "2001"
 797 }
 798
 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",
 804   month =        oct,
 805   year =         "1995"
 806 }
 807
 808 @phdthesis{miquel,
 809   author =       "Alexandre Miquel",
 810   title =        "Le {C}alcul des {C}onstructions {I}mplicite: syntaxe et s\'emantique",
 811   school =       "Universit\'e Paris 7",
 812   year =         "2001"
 813 }
 814
 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",
 819   year =         "2003"
 820 }
 821
 822 @phdthesis{Pons,
 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",
 826   year =         "1999"
 827 }
 828
 829 @phdthesis{blanqui,
 830   author =       "Fr\'ed\'eric Blanqui",
 831   title =        "Type Theory and Rewriting",
 832   school =       "Universit\'e Paris XI",
 833   year =         "2001"
 834 }
 835
 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
 840                   Substitutions",
 841   school =       "Chalmers University of Technology / G{\"o}teborg University",
 842   year =         "1995"
 843 }
 844
 845 @phdthesis{McBride,
 846   author =       "Conor McBride",
 847   title =        "Dependently Typed Functional Programs and their Proofs",
 848   school =       "University of Edinburgh",
 849   year =         "1999"
 850 }
 851
 852 @phdthesis{schena,
 853   author =       "Irene Schena",
 854   title =        "Towards a Semantic Web for Formal Mathematics",
 855   school =       "University of Bologna",
 856   year =         "2002"
 857 }
 858
 859 @phdthesis{fguidi,
 860   author = "Ferruccio Guidi",
 861   title = "Searching and Retrieving in Content-Based Repositories
 862            of Formal Mathematical Knowledge",
 863   school = "University of Bologna",
 864   month = mar,
 865   year = "2003",
 866   note = "Technical Report UBLCS 2003-06"
 867 }
 868
 869 @phdthesis{padovani,
 870   author = "Luca Padovani",
 871   title = "MathML Formatting",
 872   school = "University of Bologna",
 873   month = feb,
 874   year = "2003",
 875   note = "Technical Report UBLCS 2003-03"
 876 }
 877
 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",
 882   year =   2000
 883 }
 884
 885 @mastersthesis{zack-master,
 886   author =   "Stefano Zacchiroli",
 887   title =    "Web {s}ervices per il supporto alla dimostrazione interattiva",
 888   school =   "University of Bologna",
 889   year =     2003
 890 }
 891
 892 @mastersthesis{dilena,
 893   author =   "Pietro Dilena",
 894   title =    "Generazione automatica di stylesheet per notazione matematica",
 895   school =   "University of Bologna",
 896   year =     2003
 897 }
 898
 899 @phdthesis{munoz,
 900   author =       "C\'esar Munoz",
 901   title =        "A Calculus of Substitutions for Incomplete-Proof
 902                   Representation in Type Theory",
 903   school =       "INRIA",
 904   month =        nov,
 905   year =         "1997"
 906 }
 907
 908 @phdthesis{strecker,
 909   author =       "Martin Strecker",
 910   title =        "Construction and Deduction in Type Theories",
 911   school =       "Universit{\"a}t Ulm",
 912   year =         1998
 913 }
 914
 915
 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"
 920 }
 921
 922 @misc{debrujinfactor,
 923  title = "The ``de Bruijn factor''",
 924  howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}",
 925  author = "Freek Wiedijk",
 926 }
 927
 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"
 932 }
 933
 934 @misc{ALF,
 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}",
 938  key = "ALF"
 939 }
 940
 941 @misc{Coq,
 942  title = "The {C}oq proof-assistant",
 943  howpublished = "\\\url{http://coq.inria.fr}",
 944  key = "Coq"
 945 }
 946
 947 @misc{phox,
 948  title = "The {PhoX} proof-assistant",
 949  howpublished = "\\\url{http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html}",
 950  key = "PhoX"
 951 }
 952
 953 @misc{lego,
 954  title = "The {L}ego proof-assistant",
 955  howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}",
 956  url = "\url{http://www.dcs.ed.ac.uk/home/lego/}",
 957  key = "Lego"
 958 }
 959
 960 @misc{ALFA,
 961  title = "The {A}lfa proof editor",
 962  howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
 963  url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
 964  key = "Alfa"
 965 }
 966
 967 @misc{pvs,
 968  title = "The {PVS} Specification and Verification System",
 969  howpublished = "\\\url{http://pvs.csl.sri.com/}",
 970  key = "PVS"
 971 }
 972
 973 @misc{isabelle,
 974  title = "The {Isabelle} proof-assistant",
 975  howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}",
 976  key = "Isabelle"
 977 }
 978
 979 @misc{nuprl,
 980  title = "The {NuPRL} proof-assistant",
 981  howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
 982  key = "NuPRL"
 983 }
 984
 985 @misc{hollight,
 986  title = "The {HOL Light} proof-assistant",
 987  howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}",
 988  key = "HOL-Light"
 989 }
 990
 991 @misc{monet,
 992  title = "The {MONET} project",
 993  howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}",
 994  key = "Monet"
 995 }
 996
 997 @misc{calculemus,
 998  title = "The {CALCULEMUS} project",
 999  howpublished = "\url{http://www.calculemus.net/}",
1000  url = "\url{http://www.calculemus.net/}",
1001  key = "Calculemus"
1002 }
1003
1004 @misc{mizar,
1005  title = "The {M}izar proof-assistant",
1006  howpublished = "\\\url{http://mizar.uwb.edu.pl/}",
1007  key = "Mizar"
1008 }
1009
1010 @misc{openmath,
1011  howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium",
1012  author = "O. Caprotti and D. P. Carlisle and A. M. Cohen",
1013  title = "{\emph{The {O}pen{M}ath {S}tandard}}"
1014 }
1015
1016 @misc{mathml,
1017  title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
1018  editor="{Patrick Ion} and others",
1019  howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
1020  url = "\url{http://www.w3.org/TR/MathML2}",
1021  key = "Mathematical"
1022 }
1023
1024 @misc{xml,
1025  title = "{E}xtensible {M}arkup {L}anguage ({XML}).  {V}ersion 1.0.",
1026 editor="{Tim Bray} and others",
1027  howpublished = "W3C Recommendation 10 February 1998,
1028                  \url{http://www.w3.org/TR/REC-xml}",
1029  url = "\url{http://www.w3.org/TR/REC-xml}",
1030  key = "Extensible"
1031 }
1032
1033 @misc{dom,
1034  title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0",
1035  howpublished = "W3C Candidate Recommendation 10 May 2000,
1036                  \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1037  url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1038  key = "Document"
1039 }
1040
1041 @misc{URIs,
1042  title = "Universal Resource Identifiers in {WWW}",
1043  howpublished = "RFC 1630, CERN",
1044  month = jun,
1045  year = "1994",
1046  key = "URI"
1047 }
1048
1049 @misc{xpath,
1050  title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0",
1051  howpublished = "W3C Recommendation, 16 November 1999,
1052                  \url{http://www.w3.org/TR/xpath}",
1053  url = "\url{http://www.w3.org/TR/xpath}",
1054  key = "XML"
1055 }
1056
1057 @misc{xslt,
1058  title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0",
1059  howpublished = "W3C Recommendation, 16 November 1999,
1060                  \url{http://www.w3.org/TR/xslt}",
1061  url = "\url{http://www.w3.org/TR/xslt}",
1062  key = "XSLT"
1063 }
1064
1065 @misc{rdf,
1066  title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax
1067           Specification",
1068  howpublished = "W3C Recommendation 22 February 1999,
1069                  \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1070  url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1071  key = "Resource"
1072 }
1073
1074 @misc{omdoc,
1075  title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)",
1076  howpublished = "\\\url{http://www.mathweb.org/omdoc/omdoc.ps}",
1077  key = "OMDoc"
1078 }
1079
1080 @misc{FORMAVIE,
1081  title = "The {F}ormavie project",
1082  howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1083  url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1084  key = "Formavie"
1085 }
1086
1087 @misc{EHELM,
1088  title = "The {HELM} project",
1089  howpublished = "\url{http://helm.cs.unibo.it}",
1090  url = "\url{http://helm.cs.unibo.it}",
1091  key = "HELM"
1092 }
1093
1094 @misc{helm-library,
1095  title = "The {HELM} On-Line Library",
1096  howpublished = "\url{http://helm.cs.unibo.it/library.html}",
1097  url = "\url{http://helm.cs.unibo.it/library.html}",
1098  key = "HELM Library"
1099 }
1100
1101 @misc{MATHWEB,
1102  title = "The {M}ath{W}eb project",
1103  howpublished = "\url{http://www.mathweb.org}",
1104  url = "\url{http://www.mathweb.org}",
1105  key = "MathWeb"
1106 }
1107
1108 @misc{PCOQ,
1109  title = "The {PC}oq project",
1110  howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1111  url = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1112  key = "PCoq"
1113 }
1114
1115 @TechReport{HELM,
1116   author =       "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen
1117                   and Irene Schena",
1118   title =        "Towards a library of formal mathematics",
1119   year =         "2000",
1120   note =         "Panel session of the 13th {I}nternation {C}onference on
1121                   {T}heorem {P}roving in {H}igher {O}rder {L}ogics
1122                   ({TPHOLS}'2000), Portland, Oregon, USA",
1123 }
1124
1125 @TechReport{ctcoq2,
1126   author =       "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
1127   title =        "Real Theorem Provers Deserve Real User-Interfaces",
1128   month =        may,
1129   year =         "1992",
1130   institution =  "INRIA",
1131   number =       "{Inria Research Report 1684}"
1132 }
1133
1134 @inproceedings{Ring,
1135   author =       "Samuel Boutin",
1136   title =        "Using Reflection to Build Efficient and Certified Decision
1137                   Procedures",
1138   editor =       "Martin Abadi and Takahashi Ito editors",
1139   booktitle =    "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1140   pages =        "515-529",
1141   volume =       "1281",
1142   publisher =    "Springer-Verlag",
1143   year =         "1997",
1144 }
1145
1146 @inproceedings{werner-zfc,
1147   author =       "Benjamin Werner",
1148   title =        "Sets in Types, Types in Sets",
1149   editor =       "Martin Abadi and Takahashi Ito editors",
1150   booktitle =    "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1151   pages =        "530-546",
1152   volume =       "1281",
1153   publisher =    "Springer-Verlag",
1154   year =         "1997",
1155 }
1156
1157 @article{aczel,
1158   author = "Peter Aczel",
1159   title = "On Relating Type Theories and Set Theories",
1160   journal = "Lecture Notes in Computer Science",
1161   volume = "1657",
1162   year = "1999",
1163 }
1164
1165 @inproceedings{remathematization,
1166   author =       "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1167   title =        "{XML}, Stylesheets and the re-mathematization of Formal Content",
1168   booktitle =    "EXTREME",
1169   year = "2001",
1170 }
1171
1172
1173 @phdthesis{YANNTHESIS,
1174   author =       "Yann Coscoy",
1175   title =        "Explication textuelle de preuves pour le {C}alcul des
1176                   {C}onstructions {I}nductives",
1177   school =       "Universit\'e de Nice-Sophia Antipolis",
1178   year =         "2000",
1179 }
1180
1181 @phdthesis{Lippi,
1182   author =  "Sylvain Lippi",
1183   title =   "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)",
1184   school =  "Universit\'e Aix-Marseille 2",
1185   year =    "2002"
1186 }
1187
1188 @phdthesis{Werner,
1189   author =       "Benjamin Werner",
1190   title =        "Une Th\'eorie des {C}onstructions {I}nductives",
1191   school =       "Universit\'e Paris VII",
1192   month =        may,
1193   year =         "1994",
1194 }
1195
1196 @InCollection{Felleisen87,
1197   author =       "M. Felleisen and D. Friedman",
1198   editor =       "M. Wirsing",
1199   title =        "Control operators, the {SECD}-machine, and the lambda calculus",
1200   booktitle =    "Formal Description of Programming Concepts III",
1201   pages =        "193--217",
1202   publisher =    "Elsevier Science Publishers B.V.",
1203   address =      "(North-Holland) Amsterdam",
1204   year =         "1987",
1205 }
1206
1207 @TechReport{yarrow,
1208   author =       "Jan Zwanenburg",
1209   institution =  "Eindhoven University of Technology",
1210   number =       "Computing Science Report CS-98-11",
1211   title =        "The Proof-assistant Yarrow",
1212   year =         "1998"
1213 }
1214
1215 @TechReport{Ager2003a,
1216   author =       "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1217   institution =  "BRICS",
1218   month =        mar,
1219   number =       "BRICS RS-03-13",
1220   title =        "A Functional Correspondence between Evaluators and Abstract Machines",
1221   year =         "2003"
1222 }
1223
1224 @TechReport{Ager2003b,
1225   author =       "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1226   institution =  "BRICS",
1227   month =        mar,
1228   number =       "BRICS RS-03-14",
1229   title =        "From Interpreter to Compiler and Virtual Machine: A Functional Derivation",
1230   year =         "2003"
1231 }
1232
1233 @article{harperpollack,
1234   author =       "Robert Harper and Robert Pollack",
1235   title =        "Type checking with universes",
1236   journal =      "Theoretical Computer Science",
1237   volume =       "89",
1238   pages =        "107--136",
1239   year =         "1991"
1240 }
1241
1242 @article{activemath,
1243   author =       "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich",
1244   title =        "Knowledge Representation and Management in {ActiveMath}",
1245   journal =      "Annals of Mathematics and Artificial Intelligence",
1246   volume =       "38(1-3)",
1247   pages =        "47--64",
1248   month =        may,
1249   year =         "2003"
1250 }
1251
1252 @article{mkm-helm,
1253   author =       "Andrea Asperti and Ferruccio Guidi and Luca Padovani and
1254                   Claudio Sacerdoti Coen and Irene Schena",
1255   title =        "Mathematical Knowledge Management in {HELM}",
1256   journal =      "Annals of Mathematics and Artificial Intelligence",
1257   volume =       "38(1-3)",
1258   pages =        "27--46",
1259   month =        may,
1260   year =         "2003"
1261 }
1262
1263 @unpublished{formal-topology,
1264    author = "Giovanni Sambin",
1265    title = "Some points in formal topology",
1266    note = "To appear in Theoretical Computer Science",
1267    year = "2002"
1268 }
1269
1270 @TechReport{JohnHarrison:complexity-of-floating-point-proofs,
1271   author =       "John Harrison",
1272   title =        "Real Numbers in Real Applications",
1273   note =    "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002",
1274   institution =  "NASA",
1275   number =       "NASA/CP-2002-211736",
1276   year =         "2002"
1277 }
1278
1279 @inproceedings{kohlhase-anghelache,
1280   author = "Michael Kohlhase and Romeo Anghelache",
1281   title = "Towards Collaborative Content Management And Version Control For
1282            Structured Mathematical Knowledge",
1283   editor =       "Andrea Asperti and Bruno Buchberger and James H. Davenport",
1284   booktitle =    "Proceedings of the Second International Conference on
1285                   Mathematical Knowledge Management, MKM 2003",
1286   pages =        "147--161",
1287   volume =       "LNCS, 2594",
1288   publisher =    "Springer-Verlag",
1289   year =         "2003",
1290 }
1291
1292 %%% Unused entries from my Master dissertation bibliography
1293
1294 @misc{sgml,
1295         title="{Standard Generalized Markup Language (SGML)}",
1296         note="ISO 8879:1986",
1297         key="ISO"
1298         }
1299
1300 @unpublished{helm1,
1301   author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1302   title = "{Content Centric Logical Environments}",
1303   note = "Short Presentation at LICS 2000",
1304   ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz",
1305 }
1306
1307 @unpublished{helm4,
1308   author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1309   title = "{Formal Mathematics in MathML}",
1310   note = "To be presented at MathML International Conference 2000",
1311 }
1312
1313 @unpublished{helm2,
1314   author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1315   title = "{Towards a Library of Formal Mathematics}",
1316   note = "Accepted at TPHOLS 2000",
1317   ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz",
1318 }
1319
1320 @techreport{mowgli:D4a,
1321     author          = "Hanane Naciri and Luca Padovani",
1322     title           = "{MathML} Rendering/Browsing Engine",
1323     type            = {MoWGLI Report},
1324     number          = {D4a},
1325     year            = 2003,
1326     howpublished    = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}"
1327 }
1328
1329 @techreport{hazewinkel,
1330     author          = "Michiel Hazewinkel",
1331     title           = "Dynamic stochastic models for indexes and thesauri,
1332                        identification clouds, and information retrieval and
1333                        storage",
1334     type            = "{MKM Net Report}",
1335     howpublished    = "\url{http://monet.nag.co.uk/mkm//index.html}"
1336 }
1337
1338 @techreport{BarrasB:coqpar,
1339     author          = "{Barras B.} and {Boutin S.} and {Cornes C.}
1340         and {Courant J.} and {Filliatre J. C.}
1341         and {Gim\'enez E.} and {Herbelin H.} and {Huet G.}
1342         and {Munoz C.} and {Murthy C.} and {Parent C.}
1343         and {Paulin-Mohring C.} and {Saibi A.}
1344         and {Werner B.}",
1345     title           = "{The Coq Proof Assistant Reference Manual : Version
1346         6.1}",
1347     institution     = {Inria (Institut National de Recherche en Informatique
1348         et en Automatique), France},
1349     type            = {Technical Report},
1350     number          = {RT-0203},
1351     year            = 1997,
1352     author_acronym  = {WernerB},
1353     bibdate         = {May 1, 1997},
1354     source          = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/},
1355     source-date     = {Mon 11 Sep 100},
1356     title_acronym   = {coqpar}
1357 }
1358
1359 @unpublished{bw:1997,
1360   author = "Bruno Barras and Benjamin Werner",
1361   title = "{Coq in Coq}",
1362   year = "1997",
1363   note = "Submitted",
1364   ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz",
1365 }
1366
1367 @unpublished{berners-lee:1989,
1368   author = "Tim Berners-Lee",
1369   title = "{Information Management: A Proposal}",
1370   year = "1989",
1371   ps = "http://www.w3.org/History/1989/proposal.html",
1372 }
1373
1374 @techreport{natural,
1375     author          = "Yann Coscoy and Gilles Kahn and Laurent Thery",
1376     title           = "{Extracting Text from Proofs}",
1377     institution     = {Inria (Institut National de Recherche en Informatique
1378         et en Automatique), France},
1379     type            = {Technical Report},
1380     number          = {RR-2459},
1381     year            = 1995
1382 }
1383
1384 @inproceedings{Bru80,
1385         author          = "de Bruijn, N. G.",
1386         title           = "{A survey of the project AUTOMATH}",
1387         pages           = "589--606",
1388         editor          = "J. P. Seldin and J. R. Hindley",
1389         booktitle       = "To H. B. Curry: Essays in Combinatory Logic,
1390                            Lambda Calculus and Formalism",
1391         year            = 1980,
1392         publisher       = "Academic Press"
1393 }
1394
1395 @techreport{tutrect,
1396     author          = "E Gim\'enez",
1397     title           = "{A Tutorial on Recursive Types in Coq}",
1398     institution     = {Inria (Institut National de Recherche en Informatique
1399         et en Automatique), France},
1400     type            = {Technical Report},
1401     number          = {RT-0221},
1402     year            = 1998
1403 }
1404
1405 @inproceedings{QED,
1406         author          = "John Harrison",
1407         title           = "{The QED Manifesto}",
1408         pages           = "238--251",
1409         booktitle       = "Automated Deduction - CADE 12",
1410         series          = "Lecture Notes in Artificial Intelligence",
1411         volume          = 814,
1412         year            = 1994,
1413         publisher       = "Springer-Verlag"
1414 }
1415
1416 @inproceedings{harrison-mizar,
1417         author          = "John Harrison",
1418         title           = "{A Mizar Mode for HOL}",
1419         pages           = "203--220",
1420         editor          = "Joakim von Wright and Jim Grundy and John Harrison",
1421         booktitle       = "Theorem Proving in Higher Order Logics:
1422                            9th International Conference, TPHOLs'96",
1423         series          = "Lecture Notes in Computer Science",
1424         volume          = 1125,
1425         address         = "Turku, Finland",
1426         date            = "26--30 August 1996",
1427         year            = 1996,
1428         publisher       = "Springer-Verlag"
1429 }
1430
1431 @inproceedings{proverb,
1432         author="H. Horacek",
1433         title="{Presenting Proofs in a Human Oriented Way}",
1434         booktitle="16th International Conference on Automated Deduction",
1435         year="1999"
1436         }
1437
1438 @misc{HuetG:coqpat,
1439     author          = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring",
1440     title           = "{The Coq Proof Assistant. A Tutorial}",
1441     year            = 1998
1442 }
1443
1444 @PHDTHESIS{BJ94,
1445   author="{Jutting van L. S. B.}",
1446   school = {{Eindhoven University of Technology}},
1447   title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}",
1448   type = {Ph D. thesis},
1449   note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}",
1450   year = {1994}
1451 }
1452
1453 @misc{abriefhistoryoftheinternet,
1454         author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.}
1455          and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.}
1456          and {Postel J.} and {Roberts L. G.} and {Wolff S.}",
1457         title="{A Brief Hystory of the Internet}",
1458         note="http://www.isoc.org/internet-history/brief.html"
1459         }
1460
1461 @inproceedings{MacKenzie:1995,
1462         author="{MacKenzie D.}",
1463         title="{The automation of proof: A historical and sociological exploration}",
1464         booktitle="IEEE: Annals of the History of Computing",
1465         year="1995"
1466 }
1467
1468 @PHDTHESIS{Moh89b,
1469   author = "Christine Paulin-Mohring",
1470   month = {January},
1471   school = {{Paris 7}},
1472   title = "{Extraction de programmes dans le Calcul des Constructions}",
1473   type = {Th\`ese d'universit\'e},
1474   year = {1989},
1475   url = {http://www.lri.fr/~paulin/these.ps.gz},
1476 }
1477
1478 @MASTERTHESIS{ri99,
1479   author = "A. Ricci",
1480   school = {{Universit\`a degli studi di Bologna}},
1481   title = "{Studio e progettazione di un modello RDF per biblioteche matematiche
1482 elettroniche}",
1483   type = {Tesi universitaria},
1484   year = {1999}
1485 }
1486
1487 @inproceedings{Rob65,
1488         author="{Robinson J. A.}",
1489   title = "{A machine-oriented logic based on the resolution principle}",
1490   pages           = "23--41",
1491   booktitle       = "Journal of the ACM",
1492         volume = "2",
1493         year ="1965"
1494 }
1495
1496 @inproceedings{sh:1995,
1497         author="{Saibi A.} and {Huet G.}",
1498         title="{Constructive Category Theory}",
1499         booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory",
1500         address="Goteborg (Sweden)",
1501         month="January",
1502         year="1995"
1503         }
1504
1505 @inproceedings{ranta2,
1506         author="Thomas Hallgren and Aarne Ranta",
1507         title="An extensible proof text editor",
1508   BOOKTITLE = {LPAR'2000},
1509   SERIES = {LNCS/LNAI},
1510   VOLUME = 1955,
1511   YEAR = 2000
1512         }
1513
1514 @inproceedings{werner:1997,
1515         author="Benjamin Werner",
1516         title="{Constructive Category Theory}",
1517         booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software",
1518         year="1997"
1519         }
1520