helm/papers/matita/matita.bib

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