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{mowgli-deliverables,
 923  title = "{MoWGLI} Project Deliverables",
 924  howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html}",
 925  key = "MoWGLI Deliverables"
 926 }
 927
 928 @misc{ALF,
 929  title = "The {ALF} family of proof-assistants",
 930  howpublished = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
 931  url = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
 932  key = "ALF"
 933 }
 934
 935 @misc{Coq,
 936  title = "The {C}oq proof-assistant",
 937  howpublished = "\\\url{http://coq.inria.fr}",
 938  key = "Coq"
 939 }
 940
 941 @misc{phox,
 942  title = "The {PhoX} proof-assistant",
 943  howpublished = "\\\url{http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html}",
 944  key = "PhoX"
 945 }
 946
 947 @misc{lego,
 948  title = "The {L}ego proof-assistant",
 949  howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}",
 950  url = "\url{http://www.dcs.ed.ac.uk/home/lego/}",
 951  key = "Lego"
 952 }
 953
 954 @misc{ALFA,
 955  title = "The {A}lfa proof editor",
 956  howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
 957  url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
 958  key = "Alfa"
 959 }
 960
 961 @misc{pvs,
 962  title = "The {PVS} Specification and Verification System",
 963  howpublished = "\\\url{http://pvs.csl.sri.com/}",
 964  key = "PVS"
 965 }
 966
 967 @misc{isabelle,
 968  title = "The {Isabelle} proof-assistant",
 969  howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}",
 970  key = "Isabelle"
 971 }
 972
 973 @misc{nuprl,
 974  title = "The {NuPRL} proof-assistant",
 975  howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
 976  key = "NuPRL"
 977 }
 978
 979 @misc{hollight,
 980  title = "The {HOL Light} proof-assistant",
 981  howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}",
 982  key = "HOL-Light"
 983 }
 984
 985 @misc{monet,
 986  title = "The {MONET} project",
 987  howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}",
 988  key = "Monet"
 989 }
 990
 991 @misc{calculemus,
 992  title = "The {CALCULEMUS} project",
 993  howpublished = "\url{http://www.calculemus.net/}",
 994  url = "\url{http://www.calculemus.net/}",
 995  key = "Calculemus"
 996 }
 997
 998 @misc{mizar,
 999  title = "The {M}izar proof-assistant",
1000  howpublished = "\\\url{http://mizar.uwb.edu.pl/}",
1001  key = "Mizar"
1002 }
1003
1004 @misc{openmath,
1005  howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium",
1006  author = "O. Caprotti and D. P. Carlisle and A. M. Cohen",
1007  title = "{\emph{The {O}pen{M}ath {S}tandard}}"
1008 }
1009
1010 @misc{mathml,
1011  title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
1012  editor="{Patrick Ion} and others",
1013  howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
1014  url = "\url{http://www.w3.org/TR/MathML2}",
1015  key = "Mathematical"
1016 }
1017
1018 @misc{xml,
1019  title = "{E}xtensible {M}arkup {L}anguage ({XML}).  {V}ersion 1.0.",
1020 editor="{Tim Bray} and others",
1021  howpublished = "W3C Recommendation 10 February 1998,
1022                  \url{http://www.w3.org/TR/REC-xml}",
1023  url = "\url{http://www.w3.org/TR/REC-xml}",
1024  key = "Extensible"
1025 }
1026
1027 @misc{dom,
1028  title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0",
1029  howpublished = "W3C Candidate Recommendation 10 May 2000,
1030                  \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1031  url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1032  key = "Document"
1033 }
1034
1035 @misc{URIs,
1036  title = "Universal Resource Identifiers in {WWW}",
1037  howpublished = "RFC 1630, CERN",
1038  month = jun,
1039  year = "1994",
1040  key = "URI"
1041 }
1042
1043 @misc{xpath,
1044  title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0",
1045  howpublished = "W3C Recommendation, 16 November 1999,
1046                  \url{http://www.w3.org/TR/xpath}",
1047  url = "\url{http://www.w3.org/TR/xpath}",
1048  key = "XML"
1049 }
1050
1051 @misc{xslt,
1052  title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0",
1053  howpublished = "W3C Recommendation, 16 November 1999,
1054                  \url{http://www.w3.org/TR/xslt}",
1055  url = "\url{http://www.w3.org/TR/xslt}",
1056  key = "XSLT"
1057 }
1058
1059 @misc{rdf,
1060  title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax
1061           Specification",
1062  howpublished = "W3C Recommendation 22 February 1999,
1063                  \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1064  url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1065  key = "Resource"
1066 }
1067
1068 @misc{omdoc,
1069  title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)",
1070  howpublished = "\\\url{http://www.mathweb.org/omdoc/omdoc.ps}",
1071  key = "OMDoc"
1072 }
1073
1074 @misc{FORMAVIE,
1075  title = "The {F}ormavie project",
1076  howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1077  url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1078  key = "Formavie"
1079 }
1080
1081 @misc{EHELM,
1082  title = "The {HELM} project",
1083  howpublished = "\url{http://helm.cs.unibo.it}",
1084  url = "\url{http://helm.cs.unibo.it}",
1085  key = "HELM"
1086 }
1087
1088 @misc{helm-library,
1089  title = "The {HELM} On-Line Library",
1090  howpublished = "\url{http://helm.cs.unibo.it/library.html}",
1091  url = "\url{http://helm.cs.unibo.it/library.html}",
1092  key = "HELM Library"
1093 }
1094
1095 @misc{MATHWEB,
1096  title = "The {M}ath{W}eb project",
1097  howpublished = "\url{http://www.mathweb.org}",
1098  url = "\url{http://www.mathweb.org}",
1099  key = "MathWeb"
1100 }
1101
1102 @misc{PCOQ,
1103  title = "The {PC}oq project",
1104  howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1105  url = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1106  key = "PCoq"
1107 }
1108
1109 @TechReport{HELM,
1110   author =       "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen
1111                   and Irene Schena",
1112   title =        "Towards a library of formal mathematics",
1113   year =         "2000",
1114   note =         "Panel session of the 13th {I}nternation {C}onference on
1115                   {T}heorem {P}roving in {H}igher {O}rder {L}ogics
1116                   ({TPHOLS}'2000), Portland, Oregon, USA",
1117 }
1118
1119 @TechReport{ctcoq2,
1120   author =       "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
1121   title =        "Real Theorem Provers Deserve Real User-Interfaces",
1122   month =        may,
1123   year =         "1992",
1124   institution =  "INRIA",
1125   number =       "{Inria Research Report 1684}"
1126 }
1127
1128 @inproceedings{Ring,
1129   author =       "Samuel Boutin",
1130   title =        "Using Reflection to Build Efficient and Certified Decision
1131                   Procedures",
1132   editor =       "Martin Abadi and Takahashi Ito editors",
1133   booktitle =    "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1134   pages =        "515-529",
1135   volume =       "1281",
1136   publisher =    "Springer-Verlag",
1137   year =         "1997",
1138 }
1139
1140 @inproceedings{werner-zfc,
1141   author =       "Benjamin Werner",
1142   title =        "Sets in Types, Types in Sets",
1143   editor =       "Martin Abadi and Takahashi Ito editors",
1144   booktitle =    "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1145   pages =        "530-546",
1146   volume =       "1281",
1147   publisher =    "Springer-Verlag",
1148   year =         "1997",
1149 }
1150
1151 @article{aczel,
1152   author = "Peter Aczel",
1153   title = "On Relating Type Theories and Set Theories",
1154   journal = "Lecture Notes in Computer Science",
1155   volume = "1657",
1156   year = "1999",
1157 }
1158
1159 @inproceedings{remathematization,
1160   author =       "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1161   title =        "{XML}, Stylesheets and the re-mathematization of Formal Content",
1162   booktitle =    "EXTREME",
1163   year = "2001",
1164 }
1165
1166
1167 @phdthesis{YANNTHESIS,
1168   author =       "Yann Coscoy",
1169   title =        "Explication textuelle de preuves pour le {C}alcul des
1170                   {C}onstructions {I}nductives",
1171   school =       "Universit\'e de Nice-Sophia Antipolis",
1172   year =         "2000",
1173 }
1174
1175 @phdthesis{Lippi,
1176   author =  "Sylvain Lippi",
1177   title =   "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)",
1178   school =  "Universit\'e Aix-Marseille 2",
1179   year =    "2002"
1180 }
1181
1182 @phdthesis{Werner,
1183   author =       "Benjamin Werner",
1184   title =        "Une Th\'eorie des {C}onstructions {I}nductives",
1185   school =       "Universit\'e Paris VII",
1186   month =        may,
1187   year =         "1994",
1188 }
1189
1190 @InCollection{Felleisen87,
1191   author =       "M. Felleisen and D. Friedman",
1192   editor =       "M. Wirsing",
1193   title =        "Control operators, the {SECD}-machine, and the lambda calculus",
1194   booktitle =    "Formal Description of Programming Concepts III",
1195   pages =        "193--217",
1196   publisher =    "Elsevier Science Publishers B.V.",
1197   address =      "(North-Holland) Amsterdam",
1198   year =         "1987",
1199 }
1200
1201 @TechReport{yarrow,
1202   author =       "Jan Zwanenburg",
1203   institution =  "Eindhoven University of Technology",
1204   number =       "Computing Science Report CS-98-11",
1205   title =        "The Proof-assistant Yarrow",
1206   year =         "1998"
1207 }
1208
1209 @TechReport{Ager2003a,
1210   author =       "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1211   institution =  "BRICS",
1212   month =        mar,
1213   number =       "BRICS RS-03-13",
1214   title =        "A Functional Correspondence between Evaluators and Abstract Machines",
1215   year =         "2003"
1216 }
1217
1218 @TechReport{Ager2003b,
1219   author =       "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1220   institution =  "BRICS",
1221   month =        mar,
1222   number =       "BRICS RS-03-14",
1223   title =        "From Interpreter to Compiler and Virtual Machine: A Functional Derivation",
1224   year =         "2003"
1225 }
1226
1227 @article{harperpollack,
1228   author =       "Robert Harper and Robert Pollack",
1229   title =        "Type checking with universes",
1230   journal =      "Theoretical Computer Science",
1231   volume =       "89",
1232   pages =        "107--136",
1233   year =         "1991"
1234 }
1235
1236 @article{activemath,
1237   author =       "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich",
1238   title =        "Knowledge Representation and Management in {ActiveMath}",
1239   journal =      "Annals of Mathematics and Artificial Intelligence",
1240   volume =       "38(1-3)",
1241   pages =        "47--64",
1242   month =        may,
1243   year =         "2003"
1244 }
1245
1246 @article{mkm-helm,
1247   author =       "Andrea Asperti and Ferruccio Guidi and Luca Padovani and
1248                   Claudio Sacerdoti Coen and Irene Schena",
1249   title =        "Mathematical Knowledge Management in {HELM}",
1250   journal =      "Annals of Mathematics and Artificial Intelligence",
1251   volume =       "38(1-3)",
1252   pages =        "27--46",
1253   month =        may,
1254   year =         "2003"
1255 }
1256
1257 @unpublished{formal-topology,
1258    author = "Giovanni Sambin",
1259    title = "Some points in formal topology",
1260    note = "To appear in Theoretical Computer Science",
1261    year = "2002"
1262 }
1263
1264 @TechReport{JohnHarrison:complexity-of-floating-point-proofs,
1265   author =       "John Harrison",
1266   title =        "Real Numbers in Real Applications",
1267   note =    "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002",
1268   institution =  "NASA",
1269   number =       "NASA/CP-2002-211736",
1270   year =         "2002"
1271 }
1272
1273 @inproceedings{kohlhase-anghelache,
1274   author = "Michael Kohlhase and Romeo Anghelache",
1275   title = "Towards Collaborative Content Management And Version Control For
1276            Structured Mathematical Knowledge",
1277   editor =       "Andrea Asperti and Bruno Buchberger and James H. Davenport",
1278   booktitle =    "Proceedings of the Second International Conference on
1279                   Mathematical Knowledge Management, MKM 2003",
1280   pages =        "147--161",
1281   volume =       "LNCS, 2594",
1282   publisher =    "Springer-Verlag",
1283   year =         "2003",
1284 }
1285
1286 %%% Unused entries from my Master dissertation bibliography
1287
1288 @misc{sgml,
1289         title="{Standard Generalized Markup Language (SGML)}",
1290         note="ISO 8879:1986",
1291         key="ISO"
1292         }
1293
1294 @unpublished{helm1,
1295   author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1296   title = "{Content Centric Logical Environments}",
1297   note = "Short Presentation at LICS 2000",
1298   ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz",
1299 }
1300
1301 @unpublished{helm4,
1302   author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1303   title = "{Formal Mathematics in MathML}",
1304   note = "To be presented at MathML International Conference 2000",
1305 }
1306
1307 @unpublished{helm2,
1308   author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1309   title = "{Towards a Library of Formal Mathematics}",
1310   note = "Accepted at TPHOLS 2000",
1311   ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz",
1312 }
1313
1314 @techreport{mowgli:D4a,
1315     author          = "Hanane Naciri and Luca Padovani",
1316     title           = "{MathML} Rendering/Browsing Engine",
1317     type            = {MoWGLI Report},
1318     number          = {D4a},
1319     year            = 2003,
1320     howpublished    = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}"
1321 }
1322
1323 @techreport{hazewinkel,
1324     author          = "Michiel Hazewinkel",
1325     title           = "Dynamic stochastic models for indexes and thesauri,
1326                        identification clouds, and information retrieval and
1327                        storage",
1328     type            = "{MKM Net Report}",
1329     howpublished    = "\url{http://monet.nag.co.uk/mkm//index.html}"
1330 }
1331
1332 @techreport{BarrasB:coqpar,
1333     author          = "{Barras B.} and {Boutin S.} and {Cornes C.}
1334         and {Courant J.} and {Filliatre J. C.}
1335         and {Gim\'enez E.} and {Herbelin H.} and {Huet G.}
1336         and {Munoz C.} and {Murthy C.} and {Parent C.}
1337         and {Paulin-Mohring C.} and {Saibi A.}
1338         and {Werner B.}",
1339     title           = "{The Coq Proof Assistant Reference Manual : Version
1340         6.1}",
1341     institution     = {Inria (Institut National de Recherche en Informatique
1342         et en Automatique), France},
1343     type            = {Technical Report},
1344     number          = {RT-0203},
1345     year            = 1997,
1346     author_acronym  = {WernerB},
1347     bibdate         = {May 1, 1997},
1348     source          = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/},
1349     source-date     = {Mon 11 Sep 100},
1350     title_acronym   = {coqpar}
1351 }
1352
1353 @unpublished{bw:1997,
1354   author = "Bruno Barras and Benjamin Werner",
1355   title = "{Coq in Coq}",
1356   year = "1997",
1357   note = "Submitted",
1358   ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz",
1359 }
1360
1361 @unpublished{berners-lee:1989,
1362   author = "Tim Berners-Lee",
1363   title = "{Information Management: A Proposal}",
1364   year = "1989",
1365   ps = "http://www.w3.org/History/1989/proposal.html",
1366 }
1367
1368 @techreport{natural,
1369     author          = "Yann Coscoy and Gilles Kahn and Laurent Thery",
1370     title           = "{Extracting Text from Proofs}",
1371     institution     = {Inria (Institut National de Recherche en Informatique
1372         et en Automatique), France},
1373     type            = {Technical Report},
1374     number          = {RR-2459},
1375     year            = 1995
1376 }
1377
1378 @inproceedings{Bru80,
1379         author          = "de Bruijn, N. G.",
1380         title           = "{A survey of the project AUTOMATH}",
1381         pages           = "589--606",
1382         editor          = "J. P. Seldin and J. R. Hindley",
1383         booktitle       = "To H. B. Curry: Essays in Combinatory Logic,
1384                            Lambda Calculus and Formalism",
1385         year            = 1980,
1386         publisher       = "Academic Press"
1387 }
1388
1389 @techreport{tutrect,
1390     author          = "E Gim\'enez",
1391     title           = "{A Tutorial on Recursive Types in Coq}",
1392     institution     = {Inria (Institut National de Recherche en Informatique
1393         et en Automatique), France},
1394     type            = {Technical Report},
1395     number          = {RT-0221},
1396     year            = 1998
1397 }
1398
1399 @inproceedings{QED,
1400         author          = "John Harrison",
1401         title           = "{The QED Manifesto}",
1402         pages           = "238--251",
1403         booktitle       = "Automated Deduction - CADE 12",
1404         series          = "Lecture Notes in Artificial Intelligence",
1405         volume          = 814,
1406         year            = 1994,
1407         publisher       = "Springer-Verlag"
1408 }
1409
1410 @inproceedings{harrison-mizar,
1411         author          = "John Harrison",
1412         title           = "{A Mizar Mode for HOL}",
1413         pages           = "203--220",
1414         editor          = "Joakim von Wright and Jim Grundy and John Harrison",
1415         booktitle       = "Theorem Proving in Higher Order Logics:
1416                            9th International Conference, TPHOLs'96",
1417         series          = "Lecture Notes in Computer Science",
1418         volume          = 1125,
1419         address         = "Turku, Finland",
1420         date            = "26--30 August 1996",
1421         year            = 1996,
1422         publisher       = "Springer-Verlag"
1423 }
1424
1425 @inproceedings{proverb,
1426         author="H. Horacek",
1427         title="{Presenting Proofs in a Human Oriented Way}",
1428         booktitle="16th International Conference on Automated Deduction",
1429         year="1999"
1430         }
1431
1432 @misc{HuetG:coqpat,
1433     author          = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring",
1434     title           = "{The Coq Proof Assistant. A Tutorial}",
1435     year            = 1998
1436 }
1437
1438 @PHDTHESIS{BJ94,
1439   author="{Jutting van L. S. B.}",
1440   school = {{Eindhoven University of Technology}},
1441   title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}",
1442   type = {Ph D. thesis},
1443   note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}",
1444   year = {1994}
1445 }
1446
1447 @misc{abriefhistoryoftheinternet,
1448         author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.}
1449          and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.}
1450          and {Postel J.} and {Roberts L. G.} and {Wolff S.}",
1451         title="{A Brief Hystory of the Internet}",
1452         note="http://www.isoc.org/internet-history/brief.html"
1453         }
1454
1455 @inproceedings{MacKenzie:1995,
1456         author="{MacKenzie D.}",
1457         title="{The automation of proof: A historical and sociological exploration}",
1458         booktitle="IEEE: Annals of the History of Computing",
1459         year="1995"
1460 }
1461
1462 @PHDTHESIS{Moh89b,
1463   author = "Christine Paulin-Mohring",
1464   month = {January},
1465   school = {{Paris 7}},
1466   title = "{Extraction de programmes dans le Calcul des Constructions}",
1467   type = {Th\`ese d'universit\'e},
1468   year = {1989},
1469   url = {http://www.lri.fr/~paulin/these.ps.gz},
1470 }
1471
1472 @MASTERTHESIS{ri99,
1473   author = "A. Ricci",
1474   school = {{Universit\`a degli studi di Bologna}},
1475   title = "{Studio e progettazione di un modello RDF per biblioteche matematiche
1476 elettroniche}",
1477   type = {Tesi universitaria},
1478   year = {1999}
1479 }
1480
1481 @inproceedings{Rob65,
1482         author="{Robinson J. A.}",
1483   title = "{A machine-oriented logic based on the resolution principle}",
1484   pages           = "23--41",
1485   booktitle       = "Journal of the ACM",
1486         volume = "2",
1487         year ="1965"
1488 }
1489
1490 @inproceedings{sh:1995,
1491         author="{Saibi A.} and {Huet G.}",
1492         title="{Constructive Category Theory}",
1493         booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory",
1494         address="Goteborg (Sweden)",
1495         month="January",
1496         year="1995"
1497         }
1498
1499 @inproceedings{ranta2,
1500         author="Thomas Hallgren and Aarne Ranta",
1501         title="An extensible proof text editor",
1502   BOOKTITLE = {LPAR'2000},
1503   SERIES = {LNCS/LNAI},
1504   VOLUME = 1955,
1505   YEAR = 2000
1506         }
1507
1508 @inproceedings{werner:1997,
1509         author="Benjamin Werner",
1510         title="{Constructive Category Theory}",
1511         booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software",
1512         year="1997"
1513         }
1514