helm/papers/matita/matita.bib

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