helm/papers/matita/matita.bib

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