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 @article{asperti-categorical-understanding,
 553   author = "Andrea Asperti",
 554   title = "A categorical understanding of environment machines",
 555   journal = "Journal of Functional Programming",
 556   volume = "2",
 557   number = "1",
 558   pages = "23--59",
 559   month = jan,
 560   year = "1992"
 561 }
 562
 563 @article{namelessdummies,
 564   author = "{N. G. de Bruijn}",
 565   title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem",
 566   journal = "Indagationes Mathematicae",
 567   volume = "34",
 568   pages = "381--392",
 569   year = "1972"
 570 }
 571
 572 @article{ctcoq1,
 573   author = "Yves Bertot",
 574   title = "The CtCoq System: Design and Architecture",
 575   journal = "Formal Aspects of Computing",
 576   volume = "11",
 577   pages = "225--243",
 578   year = "1999"
 579 }
 580
 581 @TechReport{ctcoq2,
 582   author =       "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
 583   title =        "Real Theorem Provers Deserve Real User-Interfaces",
 584   month =        may,
 585   year =         "1992",
 586   institution =  "INRIA",
 587   number =       "{Inria Research Report 1684}"
 588 }
 589
 590 @article{ctcoq3,
 591   author = "Yves Bertot and Laurent Th\'ery",
 592   title = "A Generic Approach to Building User Interfaces for Theorem Provers",
 593   journal = "Journal of Symbolic Computation",
 594   volume = "25",
 595   pages = "161--194",
 596   year = "1998"
 597 }
 598
 599 @article{mbase,
 600   author = "Michael Kohlhase and Andreas Franke",
 601   title = "{MBase}: Representing Knowledge and Context for the Integration of Mathematical Software Systems",
 602   journal = "Journal of Symbolic Computation",
 603   volume = "32",
 604   number = "4",
 605   pages = "365--402",
 606   year = "2001",
 607   url = "\url{http://citeseer.nj.nec.com/kohlhase00mbase.html}"
 608 }
 609
 610 @inproceedings{mizarql,
 611   author = "Grzegorz Bancerek and Piotr Rudnicki",
 612   title = "Information Retrieval in {MML}",
 613   editor =       "Andrea Asperti and Bruno Buchberger and James H. Davenport",
 614   booktitle =    "Proceedings of the Second International Conference on
 615                   Mathematical Knowledge Management, MKM 2003",
 616   pages =        "119--132",
 617   volume =       "LNCS, 2594",
 618   publisher =    "Springer-Verlag",
 619   year =         "2003",
 620 }
 621
 622 @article{codedcontexttrees,
 623   author = "Harald Ganzinger and Robert Nieuwehuis and Pilar Nivela",
 624   title = "Fast Term Indexing with Coded Context Trees. Journal of Automated Reasoning",
 625   journal = "Journal of Automated Reasoning",
 626   year = "To appear"
 627 }
 628
 629 @article{ranta,
 630   author = "Aarne Ranta",
 631   title = "Grammatical Framework: A Type-Theoretical Grammar Formalism",
 632   journal = "Journal of Functional Programming",
 633   year = "To appear",
 634   note = "Manuscript made available in September 2002"
 635 }
 636
 637 @book{DiCosmo,
 638   AUTHOR = "Di Cosmo, Roberto",
 639   TITLE = {Isomorphisms of types: from $\lambda$-calculus to  information retrieval and language design},
 640   SERIES = {Progress in Theoretical Computer Science},
 641   PUBLISHER = {Birkhauser},
 642   YEAR = {1995},
 643   NOTE = {ISBN-0-8176-3763-X}
 644 }
 645
 646 @book{automath,
 647   EDITOR = "R.P. Nederpelt and J.H. Geuvers and R.C. de Vrijer",
 648   TITLE = {Selected Papers on Automath},
 649   SERIES = {Studies in Logic and the Foundations of Mathematics},
 650   PUBLISHER = {Elsevier Science},
 651   VOLUME = "133",
 652   YEAR = {1994},
 653   NOTE = {ISBN-0444898220}
 654 }
 655
 656 @misc{krivine,
 657  author = "Jean-Louis Krivine",
 658  title = "Un interpr\`ete du $\lambda$-calcul",
 659  howpublished = "Brouillon. Available on-line at \url{http://www.logique.jussieu.fr/~krivine}",
 660  year = 1985
 661 }
 662
 663 @misc{na-mkm1,
 664  title = "Progress Report: Building Interactive Digital Libraries of Formal
 665           Algorithmic Knowledge",
 666  howpublished = "Cornell University, \url{http://www.cs.uwyo.edu/~nuprl/documents/cornell_slides.pdf}",
 667  month = may,
 668  year = 2002,
 669  key = "Progress"
 670 }
 671
 672 @misc{metadata4education,
 673  title = "{L}earning {O}bject {M}etadata Standard",
 674  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+",
 675  year = 2002,
 676  key = "Learning"
 677 }
 678
 679 @misc{openmath-cd-with-plus,
 680  title = "Arith1 {OpenMath} {C}ontent {D}ictionary",
 681  howpublished = "The OpenMath Society, \url{http://www.openmath.org/cocoon/openmath/cd/arith1.ocd}",
 682  year = 2002,
 683  key = "Arith1 OpenMath Content Dictionary"
 684 }
 685
 686
 687 @misc{ddc,
 688  title = "Dewey Decimal Classification",
 689  howpublished = "\url{http://www.oclc.org/dewey}",
 690  url = "\url{http://www.oclc.org/dewey}",
 691  key = "Dewey"
 692 }
 693
 694 @misc{lc,
 695  title = "Library of Congress Classification Scheme",
 696  howpublished = "\url{http://www.loc.gov}",
 697  url = "\url{http://www.loc.gov}",
 698  key = "Library"
 699 }
 700
 701 @misc{msc,
 702  title = "Mathematical {S}ubject {C}lassification, {A}merican {M}athematical {S}ociety",
 703  howpublished = "\url{http://www.ams.org/msc}",
 704  url = "\url{http://www.ams.org/msc}",
 705  key = "Mathematical"
 706 }
 707
 708 @InCollection{borges,
 709  author = "Jorge Luis Borges",
 710  title = "The Library of {B}abel",
 711  publisher = "Grove Press",
 712  booktitle = "Ficciones",
 713  year = 1942
 714 }
 715
 716 @inproceedings{magaud,
 717  author = "Nicolas Magaud",
 718  title = "{C}hanging {D}ata {R}epresentation within the {C}oq {S}ystem",
 719  booktitle = {TPHOLs'2003},
 720  publisher = {Springer-Verlag},
 721  volume = {LNCS, 2758},
 722  year = {2003},
 723 }
 724
 725 @inproceedings{geuvers-jojgov,
 726   author =       "Herman Geuvers and Gueorgui I. Jojgov",
 727   title =        "Open Proofs and Open Terms: A Basis for Interactive Logic",
 728   editor =       "J. Bradfield",
 729   booktitle =    "Computer Science Logic: 16th International Workshop, CLS 2002",
 730   pages =        "537-552",
 731   volume =       "LNCS, 2471",
 732   publisher =    "Springer-Verlag",
 733   month =        jan,
 734   year =         "2002"
 735 }
 736
 737 @inproceedings{mkm-structure,
 738   author =       "Koji Nakagawa and Akihiro Nomura and Masakazu Suzuki",
 739   title =        "Extraction of Logical Structure from articles in Mathematics",
 740   editor =       "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
 741   booktitle =    "Proceedings of Mathematical Knowledge Management 2004",
 742   volume =       "LNCS, 3119",
 743   pages =        "276--289",
 744   publisher =    "Springer-Verlag",
 745   year =         "2004"
 746 }
 747
 748 @inproceedings{mkm-metadata2,
 749   author =       "Andrea Asperti and Matteo Selmi",
 750   title =        "Efficient Retrieval of Mathematical Statements",
 751   editor =       "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
 752   booktitle =    "Proceedings of Mathematical Knowledge Management 2004",
 753   volume =       "LNCS, 3119",
 754   pages =        "17--31",
 755   publisher =    "Springer-Verlag",
 756   year =         "2004"
 757 }
 758
 759 @inproceedings{adams,
 760   author =       "A. A. Adams",
 761   title =        "Digitisation, Representation and Formalisation: Digital
 762                   Libraries of Mathematics.",
 763   editor =       "A. Asperti, B. Buchberger, J.H. Davenport",
 764   booktitle =    "Proceedings of Mathematical Knowledge Management 2003",
 765   volume =       "LNCS, 2594",
 766   pages =        "1--16",
 767   publisher =    "Springer-Verlag",
 768   year =         "2003"
 769 }
 770
 771 @inproceedings{maya,
 772   author =       "Serge Autexier and Dieter Hutter and Heiko Mantel and Axel Schairer",
 773   title =        "Towards an Evolutionary Formal Software-Development Using {CASL}",
 774   booktitle =    "WADT99 Selected Papers Volume",
 775   volume =       "LNCS, 1827",
 776   publisher =    "Springer-Verlag",
 777   year =         "2000"
 778 }
 779
 780 @inproceedings{how-to-extract,
 781   author =       "Lu\'is Cruz Filipe and Bas Spitters",
 782   title =        "Program Extraction from large proof developments",
 783   booktitle =    "Proceedings of TPHOLS 2003",
 784   editor =       "D. Basin and B. Wolff",
 785   volume =       "LNCS, 2758",
 786   publisher =    "Springer-Verlag",
 787   year =         "2003"
 788 }
 789
 790 @inproceedings{click-and-prove,
 791   author =       "Jean-Raymond Abrial and Dominique Cansell",
 792   title =        "Click'n {P}rove: Interactive Proofs Within Set Theory",
 793   booktitle =    "Proceedings of TPHOLS 2003",
 794   editor =       "D. Basin and B. Wolff",
 795   volume =       "LNCS, 2758",
 796   publisher =    "Springer-Verlag",
 797   year =         "2003"
 798 }
 799
 800 @inproceedings{delahaye,
 801   author =       "David Delahaye and Roberto di Cosmo",
 802   title =        "Information Retrieval in a {C}oq Proof Library using
 803                   Type Isomorphisms",
 804   booktitle =    "Proceedings of TYPES 99",
 805   volume =       "LNCS",
 806   publisher =    "Springer-Verlag",
 807   year =         "1999"
 808 }
 809
 810 @TechReport{jojgov,
 811   author =       "G. I. Jojgov",
 812   title =        "Systems for open terms: An Overview",
 813   institution =  "Technische Universiteit Eindhoven",
 814   number =       "CSR 01-03",
 815   year =         "2001"
 816 }
 817
 818 @TechReport{garrigue:implicit-arguments,
 819   author =       "Jun P. Furuse and Jacques Garrigue",
 820   title =        " A label-selective lambda-calculus with optional arguments and its compilation method",
 821   institution =  "Research Institute for Mathematical Sciences, Kyoto University",
 822   number =       "RIMS Preprint 1041",
 823   month =        oct,
 824   year =         "1995"
 825 }
 826
 827 @phdthesis{miquel,
 828   author =       "Alexandre Miquel",
 829   title =        "Le {C}alcul des {C}onstructions {I}mplicite: syntaxe et s\'emantique",
 830   school =       "Universit\'e Paris 7",
 831   year =         "2001"
 832 }
 833
 834 @phdthesis{chrzaszcz,
 835   author =       "Jacek Chrz{\c{a}}szcs",
 836   title =        "Modules in Type Theory with Generative Definitions",
 837   school =       "Uniwersytet Warszawski and Universit\'e de Paris Sud",
 838   year =         "2003"
 839 }
 840
 841 @phdthesis{Pons,
 842   author =       "Olivier Pons",
 843   title =        "Conception et r\'ealisation d'outils d'aide au d\'eveloppement de grosse th\'eories dans les syst\`emes de preuves interactifs",
 844   school =       "Conservatoire National des Arts et M\'etiers",
 845   year =         "1999"
 846 }
 847
 848 @phdthesis{blanqui,
 849   author =       "Fr\'ed\'eric Blanqui",
 850   title =        "Type Theory and Rewriting",
 851   school =       "Universit\'e Paris XI",
 852   year =         "2001"
 853 }
 854
 855 @phdthesis{magnusson,
 856   author =       "Lena Magnusson",
 857   title =        "The Implementation of {ALF} -- a Proof Editor based
 858                   on Martin-L{\"o}f Monomorphic Type Theory with Explicit
 859                   Substitutions",
 860   school =       "Chalmers University of Technology / G{\"o}teborg University",
 861   year =         "1995"
 862 }
 863
 864 @phdthesis{McBride,
 865   author =       "Conor McBride",
 866   title =        "Dependently Typed Functional Programs and their Proofs",
 867   school =       "University of Edinburgh",
 868   year =         "1999"
 869 }
 870
 871 @phdthesis{schena,
 872   author =       "Irene Schena",
 873   title =        "Towards a Semantic Web for Formal Mathematics",
 874   school =       "University of Bologna",
 875   year =         "2002"
 876 }
 877
 878 @phdthesis{fguidi,
 879   author = "Ferruccio Guidi",
 880   title = "Searching and Retrieving in Content-Based Repositories
 881            of Formal Mathematical Knowledge",
 882   school = "University of Bologna",
 883   month = mar,
 884   year = "2003",
 885   note = "Technical Report UBLCS 2003-06"
 886 }
 887
 888 @phdthesis{padovani,
 889   author = "Luca Padovani",
 890   title = "MathML Formatting",
 891   school = "University of Bologna",
 892   month = feb,
 893   year = "2003",
 894   note = "Technical Report UBLCS 2003-03"
 895 }
 896
 897 @mastersthesis{csc-master,
 898   author = "Sacerdoti Coen, Claudio",
 899   title =  "Progettazione e realizzazione con tecnologia {XML} di basi distribuite di conoscenza matematica formalizzata",
 900   school = "University of Bologna",
 901   year =   2000
 902 }
 903
 904 @mastersthesis{zack-master,
 905   author =   "Stefano Zacchiroli",
 906   title =    "Web {s}ervices per il supporto alla dimostrazione interattiva",
 907   school =   "University of Bologna",
 908   year =     2003
 909 }
 910
 911 @mastersthesis{dilena,
 912   author =   "Pietro Dilena",
 913   title =    "Generazione automatica di stylesheet per notazione matematica",
 914   school =   "University of Bologna",
 915   year =     2003
 916 }
 917
 918 @phdthesis{munoz,
 919   author =       "C\'esar Munoz",
 920   title =        "A Calculus of Substitutions for Incomplete-Proof
 921                   Representation in Type Theory",
 922   school =       "INRIA",
 923   month =        nov,
 924   year =         "1997"
 925 }
 926
 927 @phdthesis{strecker,
 928   author =       "Martin Strecker",
 929   title =        "Construction and Deduction in Type Theories",
 930   school =       "Universit{\"a}t Ulm",
 931   year =         1998
 932 }
 933
 934 @misc{content-centric,
 935  author = "Andrea Asperti and Luca padovani and Claudio Sacerdoti Coen
 936            and irene Schena",
 937  title = "Content-centric Logical Envirnoments",
 938  howpublished = "Short Presentation at the Fifteenth IEEE Symposium on Logic in Computer Science",
 939  month = "June",
 940  year = "2000",
 941  key = "content centric"
 942 }
 943
 944 @misc{mowgli-proposal,
 945  title = "The {MoWGLI Proposal}, {HTML} Version",
 946  howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/project.html}",
 947  key = "MoWGLI Proposal"
 948 }
 949
 950 @misc{debrujinfactor,
 951  title = "The ``de Bruijn factor''",
 952  howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}",
 953  author = "Freek Wiedijk",
 954 }
 955
 956 @misc{mowgli-deliverables,
 957  title = "{MoWGLI} Project Deliverables",
 958  howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html}",
 959  key = "MoWGLI Deliverables"
 960 }
 961
 962 @misc{ALF,
 963  title = "The {ALF} family of proof-assistants",
 964  howpublished = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
 965  url = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}",
 966  key = "ALF"
 967 }
 968
 969 @misc{CoqManual,
 970  title = "The {C}oq Proof Assistant Reference Manual",
 971  author = "The Coq Development Team",
 972  howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
 973  key = "CoqManual"
 974 }
 975
 976 @misc{Coq,
 977  title = "The {C}oq proof-assistant",
 978  howpublished = "\\\url{http://coq.inria.fr}",
 979  key = "Coq"
 980 }
 981
 982 @misc{phox,
 983  title = "The {PhoX} proof-assistant",
 984  howpublished = "\\\url{http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html}",
 985  key = "PhoX"
 986 }
 987
 988 @misc{lego,
 989  title = "The {L}ego proof-assistant",
 990  howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}",
 991  url = "\url{http://www.dcs.ed.ac.uk/home/lego/}",
 992  key = "Lego"
 993 }
 994
 995 @misc{ALFA,
 996  title = "The {A}lfa proof editor",
 997  howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
 998  url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}",
 999  key = "Alfa"
1000 }
1001
1002 @misc{pvs,
1003  title = "The {PVS} Specification and Verification System",
1004  howpublished = "\\\url{http://pvs.csl.sri.com/}",
1005  key = "PVS"
1006 }
1007
1008 @misc{isabelle,
1009  title = "The {Isabelle} proof-assistant",
1010  howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}",
1011  key = "Isabelle"
1012 }
1013
1014 @book{nuprl-book,
1015   author =    "Constable, Robert L. and Stuart F. Allen and H. M. Bromley and
1016                W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and
1017                T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
1018                Scott F. Smith",
1019   title =     "Implementing Mathematics with the {N}uprl Development System",
1020   publisher = "Prentice-Hall",
1021   year =      1986,
1022   address =   "NJ"
1023 }
1024
1025 @misc{nuprl,
1026  title = "The {NuPRL} proof-assistant",
1027  howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
1028  key = "NuPRL"
1029 }
1030
1031 @misc{hollight,
1032  title = "The {HOL Light} proof-assistant",
1033  howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}",
1034  key = "HOL-Light"
1035 }
1036
1037 @misc{monet,
1038  title = "The {MONET} project",
1039  howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}",
1040  key = "Monet"
1041 }
1042
1043 @misc{calculemus,
1044  title = "The {CALCULEMUS} project",
1045  howpublished = "\url{http://www.calculemus.net/}",
1046  url = "\url{http://www.calculemus.net/}",
1047  key = "Calculemus"
1048 }
1049
1050 @misc{mizar,
1051  title = "The {M}izar proof-assistant",
1052  howpublished = "\\\url{http://mizar.uwb.edu.pl/}",
1053  key = "Mizar"
1054 }
1055
1056 @misc{openmath,
1057  howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium",
1058  author = "O. Caprotti and D. P. Carlisle and A. M. Cohen",
1059  title = "{\emph{The {O}pen{M}ath {S}tandard}}"
1060 }
1061
1062 @misc{mathml,
1063  title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
1064  editor="{Patrick Ion} and others",
1065  howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
1066  url = "\url{http://www.w3.org/TR/MathML2}",
1067  key = "Mathematical"
1068 }
1069
1070 @misc{xml,
1071  title = "{E}xtensible {M}arkup {L}anguage ({XML}).  {V}ersion 1.0.",
1072 editor="{Tim Bray} and others",
1073  howpublished = "W3C Recommendation 10 February 1998,
1074                  \url{http://www.w3.org/TR/REC-xml}",
1075  url = "\url{http://www.w3.org/TR/REC-xml}",
1076  key = "Extensible"
1077 }
1078
1079 @misc{dom,
1080  title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0",
1081  howpublished = "W3C Candidate Recommendation 10 May 2000,
1082                  \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1083  url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}",
1084  key = "Document"
1085 }
1086
1087 @misc{URIs,
1088  title = "Universal Resource Identifiers in {WWW}",
1089  howpublished = "RFC 1630, CERN",
1090  month = jun,
1091  year = "1994",
1092  key = "URI"
1093 }
1094
1095 @misc{xpath,
1096  title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0",
1097  howpublished = "W3C Recommendation, 16 November 1999,
1098                  \url{http://www.w3.org/TR/xpath}",
1099  url = "\url{http://www.w3.org/TR/xpath}",
1100  key = "XML"
1101 }
1102
1103 @misc{xslt,
1104  title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0",
1105  howpublished = "W3C Recommendation, 16 November 1999,
1106                  \url{http://www.w3.org/TR/xslt}",
1107  url = "\url{http://www.w3.org/TR/xslt}",
1108  key = "XSLT"
1109 }
1110
1111 @misc{rdf,
1112  title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax
1113           Specification",
1114  howpublished = "W3C Recommendation 22 February 1999,
1115                  \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1116  url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}",
1117  key = "Resource"
1118 }
1119
1120 @misc{omdoc,
1121  title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)",
1122  howpublished = "\\\url{http://www.mathweb.org/omdoc/omdoc.ps}",
1123  key = "OMDoc"
1124 }
1125
1126 @misc{FORMAVIE,
1127  title = "The {F}ormavie project",
1128  howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1129  url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}",
1130  key = "Formavie"
1131 }
1132
1133 @misc{EHELM,
1134  title = "The {HELM} project",
1135  howpublished = "\url{http://helm.cs.unibo.it}",
1136  url = "\url{http://helm.cs.unibo.it}",
1137  key = "HELM"
1138 }
1139
1140 @misc{helm-library,
1141  title = "The {HELM} On-Line Library",
1142  howpublished = "\url{http://helm.cs.unibo.it/library.html}",
1143  url = "\url{http://helm.cs.unibo.it/library.html}",
1144  key = "HELM Library"
1145 }
1146
1147 @misc{MATHWEB,
1148  title = "The {M}ath{W}eb project",
1149  howpublished = "\url{http://www.mathweb.org}",
1150  url = "\url{http://www.mathweb.org}",
1151  key = "MathWeb"
1152 }
1153
1154 @misc{PCOQ,
1155  title = "The {PC}oq project",
1156  howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1157  url = "\url{http://www-sop.inria.fr/lemme/pcoq}",
1158  key = "PCoq"
1159 }
1160
1161 @TechReport{HELM,
1162   author =       "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen
1163                   and Irene Schena",
1164   title =        "Towards a library of formal mathematics",
1165   year =         "2000",
1166   note =         "Panel session of the 13th {I}nternation {C}onference on
1167                   {T}heorem {P}roving in {H}igher {O}rder {L}ogics
1168                   ({TPHOLS}'2000), Portland, Oregon, USA",
1169 }
1170
1171 @inproceedings{Ring,
1172   author =       "Samuel Boutin",
1173   title =        "Using Reflection to Build Efficient and Certified Decision
1174                   Procedures",
1175   editor =       "Martin Abadi and Takahashi Ito editors",
1176   booktitle =    "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1177   pages =        "515-529",
1178   volume =       "1281",
1179   publisher =    "Springer-Verlag",
1180   year =         "1997",
1181 }
1182
1183 @inproceedings{werner-zfc,
1184   author =       "Benjamin Werner",
1185   title =        "Sets in Types, Types in Sets",
1186   editor =       "Martin Abadi and Takahashi Ito editors",
1187   booktitle =    "Theoretical Aspect of Computer Software {TACS'}97, LNCS",
1188   pages =        "530-546",
1189   volume =       "1281",
1190   publisher =    "Springer-Verlag",
1191   year =         "1997",
1192 }
1193
1194 @article{aczel,
1195   author = "Peter Aczel",
1196   title = "On Relating Type Theories and Set Theories",
1197   journal = "Lecture Notes in Computer Science",
1198   volume = "1657",
1199   year = "1999",
1200 }
1201
1202 @inproceedings{remathematization,
1203   author =       "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1204   title =        "{XML}, Stylesheets and the re-mathematization of Formal Content",
1205   booktitle =    "EXTREME",
1206   year = "2001",
1207 }
1208
1209
1210 @phdthesis{YANNTHESIS,
1211   author =       "Yann Coscoy",
1212   title =        "Explication textuelle de preuves pour le {C}alcul des
1213                   {C}onstructions {I}nductives",
1214   school =       "Universit\'e de Nice-Sophia Antipolis",
1215   year =         "2000",
1216 }
1217
1218 @phdthesis{Lippi,
1219   author =  "Sylvain Lippi",
1220   title =   "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)",
1221   school =  "Universit\'e Aix-Marseille 2",
1222   year =    "2002"
1223 }
1224
1225 @phdthesis{Werner,
1226   author =       "Benjamin Werner",
1227   title =        "Une Th\'eorie des {C}onstructions {I}nductives",
1228   school =       "Universit\'e Paris VII",
1229   month =        may,
1230   year =         "1994",
1231 }
1232
1233 @InCollection{Felleisen87,
1234   author =       "M. Felleisen and D. Friedman",
1235   editor =       "M. Wirsing",
1236   title =        "Control operators, the {SECD}-machine, and the lambda calculus",
1237   booktitle =    "Formal Description of Programming Concepts III",
1238   pages =        "193--217",
1239   publisher =    "Elsevier Science Publishers B.V.",
1240   address =      "(North-Holland) Amsterdam",
1241   year =         "1987",
1242 }
1243
1244 @TechReport{yarrow,
1245   author =       "Jan Zwanenburg",
1246   institution =  "Eindhoven University of Technology",
1247   number =       "Computing Science Report CS-98-11",
1248   title =        "The Proof-assistant Yarrow",
1249   year =         "1998"
1250 }
1251
1252 @TechReport{Ager2003a,
1253   author =       "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1254   institution =  "BRICS",
1255   month =        mar,
1256   number =       "BRICS RS-03-13",
1257   title =        "A Functional Correspondence between Evaluators and Abstract Machines",
1258   year =         "2003"
1259 }
1260
1261 @TechReport{Ager2003b,
1262   author =       "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard",
1263   institution =  "BRICS",
1264   month =        mar,
1265   number =       "BRICS RS-03-14",
1266   title =        "From Interpreter to Compiler and Virtual Machine: A Functional Derivation",
1267   year =         "2003"
1268 }
1269
1270 @article{harperpollack,
1271   author =       "Robert Harper and Robert Pollack",
1272   title =        "Type checking with universes",
1273   journal =      "Theoretical Computer Science",
1274   volume =       "89",
1275   pages =        "107--136",
1276   year =         "1991"
1277 }
1278
1279 @article{activemath,
1280   author =       "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich",
1281   title =        "Knowledge Representation and Management in {ActiveMath}",
1282   journal =      "Annals of Mathematics and Artificial Intelligence",
1283   volume =       "38(1-3)",
1284   pages =        "47--64",
1285   month =        may,
1286   year =         "2003"
1287 }
1288
1289 @article{mkm-helm,
1290   author =       "Andrea Asperti and Ferruccio Guidi and Luca Padovani and
1291                   Claudio Sacerdoti Coen and Irene Schena",
1292   title =        "Mathematical Knowledge Management in {HELM}",
1293   journal =      "Annals of Mathematics and Artificial Intelligence",
1294   volume =       "38(1-3)",
1295   pages =        "27--46",
1296   month =        may,
1297   year =         "2003"
1298 }
1299
1300 @unpublished{formal-topology,
1301    author = "Giovanni Sambin",
1302    title = "Some points in formal topology",
1303    note = "To appear in Theoretical Computer Science",
1304    year = "2002"
1305 }
1306
1307 @TechReport{JohnHarrison:complexity-of-floating-point-proofs,
1308   author =       "John Harrison",
1309   title =        "Real Numbers in Real Applications",
1310   note =    "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002",
1311   institution =  "NASA",
1312   number =       "NASA/CP-2002-211736",
1313   year =         "2002"
1314 }
1315
1316 @inproceedings{kohlhase-anghelache,
1317   author = "Michael Kohlhase and Romeo Anghelache",
1318   title = "Towards Collaborative Content Management And Version Control For
1319            Structured Mathematical Knowledge",
1320   editor =       "Andrea Asperti and Bruno Buchberger and James H. Davenport",
1321   booktitle =    "Proceedings of the Second International Conference on
1322                   Mathematical Knowledge Management, MKM 2003",
1323   pages =        "147--161",
1324   volume =       "LNCS, 2594",
1325   publisher =    "Springer-Verlag",
1326   year =         "2003",
1327 }
1328
1329 %%% Unused entries from my Master dissertation bibliography
1330
1331 @misc{sgml,
1332         title="{Standard Generalized Markup Language (SGML)}",
1333         note="ISO 8879:1986",
1334         key="ISO"
1335         }
1336
1337 @unpublished{helm1,
1338   author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1339   title = "{Content Centric Logical Environments}",
1340   note = "Short Presentation at LICS 2000",
1341   ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz",
1342 }
1343
1344 @unpublished{helm4,
1345   author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1346   title = "{Formal Mathematics in MathML}",
1347   note = "To be presented at MathML International Conference 2000",
1348 }
1349
1350 @unpublished{helm2,
1351   author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
1352   title = "{Towards a Library of Formal Mathematics}",
1353   note = "Accepted at TPHOLS 2000",
1354   ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz",
1355 }
1356
1357 @techreport{mowgli:D4a,
1358     author          = "Hanane Naciri and Luca Padovani",
1359     title           = "{MathML} Rendering/Browsing Engine",
1360     type            = {MoWGLI Report},
1361     number          = {D4a},
1362     year            = 2003,
1363     howpublished    = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}"
1364 }
1365
1366 @techreport{hazewinkel,
1367     author          = "Michiel Hazewinkel",
1368     title           = "Dynamic stochastic models for indexes and thesauri,
1369                        identification clouds, and information retrieval and
1370                        storage",
1371     type            = "{MKM Net Report}",
1372     howpublished    = "\url{http://monet.nag.co.uk/mkm//index.html}"
1373 }
1374
1375 @techreport{BarrasB:coqpar,
1376     author          = "{Barras B.} and {Boutin S.} and {Cornes C.}
1377         and {Courant J.} and {Filliatre J. C.}
1378         and {Gim\'enez E.} and {Herbelin H.} and {Huet G.}
1379         and {Munoz C.} and {Murthy C.} and {Parent C.}
1380         and {Paulin-Mohring C.} and {Saibi A.}
1381         and {Werner B.}",
1382     title           = "{The Coq Proof Assistant Reference Manual : Version
1383         6.1}",
1384     institution     = {Inria (Institut National de Recherche en Informatique
1385         et en Automatique), France},
1386     type            = {Technical Report},
1387     number          = {RT-0203},
1388     year            = 1997,
1389     author_acronym  = {WernerB},
1390     bibdate         = {May 1, 1997},
1391     source          = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/},
1392     source-date     = {Mon 11 Sep 100},
1393     title_acronym   = {coqpar}
1394 }
1395
1396 @unpublished{bw:1997,
1397   author = "Bruno Barras and Benjamin Werner",
1398   title = "{Coq in Coq}",
1399   year = "1997",
1400   note = "Submitted",
1401   ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz",
1402 }
1403
1404 @unpublished{berners-lee:1989,
1405   author = "Tim Berners-Lee",
1406   title = "{Information Management: A Proposal}",
1407   year = "1989",
1408   ps = "http://www.w3.org/History/1989/proposal.html",
1409 }
1410
1411 @techreport{natural,
1412     author          = "Yann Coscoy and Gilles Kahn and Laurent Thery",
1413     title           = "{Extracting Text from Proofs}",
1414     institution     = {Inria (Institut National de Recherche en Informatique
1415         et en Automatique), France},
1416     type            = {Technical Report},
1417     number          = {RR-2459},
1418     year            = 1995
1419 }
1420
1421 @inproceedings{Bru80,
1422         author          = "de Bruijn, N. G.",
1423         title           = "{A survey of the project AUTOMATH}",
1424         pages           = "589--606",
1425         editor          = "J. P. Seldin and J. R. Hindley",
1426         booktitle       = "To H. B. Curry: Essays in Combinatory Logic,
1427                            Lambda Calculus and Formalism",
1428         year            = 1980,
1429         publisher       = "Academic Press"
1430 }
1431
1432 @techreport{tutrect,
1433     author          = "E Gim\'enez",
1434     title           = "{A Tutorial on Recursive Types in Coq}",
1435     institution     = {Inria (Institut National de Recherche en Informatique
1436         et en Automatique), France},
1437     type            = {Technical Report},
1438     number          = {RT-0221},
1439     year            = 1998
1440 }
1441
1442 @inproceedings{QED,
1443         author          = "John Harrison",
1444         title           = "{The QED Manifesto}",
1445         pages           = "238--251",
1446         booktitle       = "Automated Deduction - CADE 12",
1447         series          = "Lecture Notes in Artificial Intelligence",
1448         volume          = 814,
1449         year            = 1994,
1450         publisher       = "Springer-Verlag"
1451 }
1452
1453 @inproceedings{harrison-mizar,
1454         author          = "John Harrison",
1455         title           = "{A Mizar Mode for HOL}",
1456         pages           = "203--220",
1457         editor          = "Joakim von Wright and Jim Grundy and John Harrison",
1458         booktitle       = "Theorem Proving in Higher Order Logics:
1459                            9th International Conference, TPHOLs'96",
1460         series          = "Lecture Notes in Computer Science",
1461         volume          = 1125,
1462         address         = "Turku, Finland",
1463         date            = "26--30 August 1996",
1464         year            = 1996,
1465         publisher       = "Springer-Verlag"
1466 }
1467
1468 @inproceedings{proverb,
1469         author="H. Horacek",
1470         title="{Presenting Proofs in a Human Oriented Way}",
1471         booktitle="16th International Conference on Automated Deduction",
1472         year="1999"
1473         }
1474
1475 @misc{HuetG:coqpat,
1476     author          = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring",
1477     title           = "{The Coq Proof Assistant. A Tutorial}",
1478     year            = 1998
1479 }
1480
1481 @PHDTHESIS{BJ94,
1482   author="{Jutting van L. S. B.}",
1483   school = {{Eindhoven University of Technology}},
1484   title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}",
1485   type = {Ph D. thesis},
1486   note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}",
1487   year = {1994}
1488 }
1489
1490 @misc{abriefhistoryoftheinternet,
1491         author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.}
1492          and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.}
1493          and {Postel J.} and {Roberts L. G.} and {Wolff S.}",
1494         title="{A Brief Hystory of the Internet}",
1495         note="http://www.isoc.org/internet-history/brief.html"
1496         }
1497
1498 @inproceedings{MacKenzie:1995,
1499         author="{MacKenzie D.}",
1500         title="{The automation of proof: A historical and sociological exploration}",
1501         booktitle="IEEE: Annals of the History of Computing",
1502         year="1995"
1503 }
1504
1505 @PHDTHESIS{Moh89b,
1506   author = "Christine Paulin-Mohring",
1507   month = {January},
1508   school = {{Paris 7}},
1509   title = "{Extraction de programmes dans le Calcul des Constructions}",
1510   type = {Th\`ese d'universit\'e},
1511   year = {1989},
1512   url = {http://www.lri.fr/~paulin/these.ps.gz},
1513 }
1514
1515 @MASTERTHESIS{ri99,
1516   author = "A. Ricci",
1517   school = {{Universit\`a degli studi di Bologna}},
1518   title = "{Studio e progettazione di un modello RDF per biblioteche matematiche
1519 elettroniche}",
1520   type = {Tesi universitaria},
1521   year = {1999}
1522 }
1523
1524 @inproceedings{Rob65,
1525         author="{Robinson J. A.}",
1526   title = "{A machine-oriented logic based on the resolution principle}",
1527   pages           = "23--41",
1528   booktitle       = "Journal of the ACM",
1529         volume = "2",
1530         year ="1965"
1531 }
1532
1533 @inproceedings{sh:1995,
1534         author="{Saibi A.} and {Huet G.}",
1535         title="{Constructive Category Theory}",
1536         booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory",
1537         address="Goteborg (Sweden)",
1538         month="January",
1539         year="1995"
1540         }
1541
1542 @inproceedings{ranta2,
1543         author="Thomas Hallgren and Aarne Ranta",
1544         title="An extensible proof text editor",
1545   BOOKTITLE = {LPAR'2000},
1546   SERIES = {LNCS/LNAI},
1547   VOLUME = 1955,
1548   YEAR = 2000
1549         }
1550
1551 @inproceedings{werner:1997,
1552         author="Benjamin Werner",
1553         title="{Constructive Category Theory}",
1554         booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software",
1555         year="1997"
1556         }
1557