helm/papers/matita/matita.bib

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