helm/papers/matita/matita.bib

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