helm/papers/matita/matita.bib

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