Warning, /office/kbibtex-testset/bib/in-the-wild/imps-bibliography.bib is written in an unsupported language. File is not indexed.
0001 %% This file is a complete bibliography of the papers on IMPS in
0002 %% BibTeX format. Send questions to wmfarmer at mcmaster.ca.
0003
0004 @TechReport{Farmer87,
0005 author = "W. M. Farmer",
0006 title = "Abstract Data Types in Many-Sorted Second-Order Logic",
0007 institution = "The {MITRE} Corporation",
0008 year = "1987",
0009 OPTtype = "",
0010 number = "M87-64",
0011 OPTaddress = "202 Burlington Road, Bedford, MA 01730-1420, USA",
0012 OPTmonth = "",
0013 OPTnote = ""
0014 }
0015
0016 @Article{Farmer90,
0017 author = "W. M. Farmer",
0018 title = "A Partial Functions Version of {Church's} Simple
0019 Theory of Types",
0020 journal = "Journal of Symbolic Logic",
0021 year = "1990",
0022 volume = "55",
0023 Optnumber = "3",
0024 pages = "1269--91",
0025 OPTmonth = "",
0026 OPTnote = "Also {MITRE} Corporation technical report M88-52,
0027 1988; revised 1990."
0028 }
0029
0030 @Article{Farmer93b,
0031 author = "W. M. Farmer",
0032 title = "A Simple Type Theory with Partial Functions and Subtypes",
0033 journal = "Annals of Pure and Applied Logic",
0034 year = "1993",
0035 volume = "64",
0036 OPTnumber = "3",
0037 pages = "211--240",
0038 OPTmonth = "",
0039 OPTnote = ""
0040 }
0041
0042 @InProceedings{Farmer94,
0043 author = "W. M. Farmer",
0044 title = "Theory Interpretation in Simple Type Theory",
0045 booktitle = "Higher-Order Algebra, Logic, and Term Rewriting",
0046 year = "1994",
0047 series = "Lecture Notes in Computer Science",
0048 volume = "816",
0049 editor = "J. Heering et al.",
0050 pages = "96--123",
0051 publisher = "Springer-Verlag",
0052 OPTnote = ""
0053 }
0054
0055 @TechReport{Farmer94a,
0056 author = "W. M. Farmer",
0057 title = "A General Method for Safely Overwriting Theories in
0058 Mechanized Mathematics Systems",
0059 institution = "The {MITRE} Corporation",
0060 year = "1994",
0061 OPTtype = "",
0062 OPTnumber = "",
0063 OPTaddress = "202 Burlington Road, Bedford, MA 01730-1420, USA",
0064 OPTmonth = "",
0065 OPTnote = "Revised version of the technical report ``A
0066 technique for safely extending axiomatic theories''."
0067 }
0068
0069 @Article{Farmer95,
0070 author = "W. M. Farmer",
0071 title = "Reasoning about Partial Functions with the Aid of a
0072 Computer",
0073 OPTcrossref = "",
0074 OPTkey = "",
0075 journal = "Erkenntnis",
0076 year = "1995",
0077 volume = "43",
0078 OPTnumber = "3",
0079 pages = "279--294",
0080 OPTmonth = "",
0081 OPTnote = "",
0082 OPTannote = "",
0083 patron = "Farmer"
0084 }
0085
0086 @InProceedings{Farmer96,
0087 author = {W. M. Farmer},
0088 title = {Mechanizing the Traditional Approach to Partial Functions},
0089 booktitle = {CADE-13 Workshop on the Mechanization of
0090 Partial Functions},
0091 OPTcrossref = {},
0092 OPTkey = {},
0093 pages = {27--32},
0094 year = {1996},
0095 editor = {W.~Farmer and M.~Kerber and M.~Kohlhase},
0096 OPTvolume = {},
0097 OPTnumber = {},
0098 OPTseries = {},
0099 OPTaddress = {},
0100 OPTmonth = {July},
0101 OPTorganization = {},
0102 OPTpublisher = {},
0103 OPTnote = {},
0104 OPTannote = {}
0105 }
0106
0107 @InProceedings{Farmer98,
0108 author = {W. M. Farmer},
0109 title = {{STMM} and Partial Functions},
0110 booktitle = {CADE-15 Workshop on the Mechanization of
0111 Partial Functions},
0112 OPTcrossref = {},
0113 OPTkey = {},
0114 pages = {3--14},
0115 year = {1998},
0116 editor = {M.~Kerber},
0117 OPTvolume = {},
0118 OPTnumber = {},
0119 OPTseries = {},
0120 OPTaddress = {},
0121 OPTmonth = {July},
0122 OPTorganization = {},
0123 OPTpublisher = {},
0124 OPTnote = {},
0125 OPTannote = {}
0126 }
0127
0128 @InProceedings{Farmer98a,
0129 author = {W. M. Farmer},
0130 title = {The Interactive Mathematics Laboratory},
0131 booktitle = {Proceedings of the 31st Annual Midwest Instruction
0132 and Computing Symposium (MICS '98)},
0133 OPTcrossref = {},
0134 OPTkey = {},
0135 pages = {16--18},
0136 year = {1998},
0137 OPTeditor = {},
0138 OPTvolume = {},
0139 OPTnumber = {},
0140 OPTseries = {},
0141 OPTaddress = {},
0142 month = {April},
0143 OPTorganization = {},
0144 OPTpublisher = {},
0145 OPTnote = {},
0146 OPTannote = {}
0147 }
0148
0149 @InProceedings{Farmer99,
0150 author = {W. M. Farmer},
0151 title = {A Scheme for Defining Partial Higher-Order
0152 Functions by Recursion},
0153 booktitle = {3rd Irish Workshop on Formal Methods},
0154 OPTcrossref = {},
0155 OPTkey = {},
0156 OPTpages = {},
0157 year = {1999},
0158 OPTeditor = {},
0159 OPTvolume = {},
0160 OPTnumber = {},
0161 series = {electronic Workshops in Computing, \url{http://ewic.org.uk/workshops}},
0162 OPTaddress = {},
0163 OPTmonth = {},
0164 OPTorganization = {},
0165 OPTpublisher = {},
0166 OPTnote = {},
0167 OPTannote = {}
0168 }
0169
0170 @InProceedings{Farmer00,
0171 author = "W. M. Farmer",
0172 title = "An Infrastructure for Intertheory Reasoning",
0173 booktitle = "Automated Deduction---CADE-17",
0174 year = "2000",
0175 series = "Lecture Notes in Computer Science",
0176 volume = "1831",
0177 editor = "D. McAllester",
0178 pages = "115--131",
0179 OPTorganization = "",
0180 publisher = "Springer-Verlag",
0181 OPTaddress = "",
0182 OPTmonth = "",
0183 OPTnote = ""
0184 }
0185
0186 @InProceedings{Farmer00a,
0187 author = {W. M. Farmer},
0188 title = {A Proposal for the Development of an Interactive
0189 Mathematics Laboratory for Mathematics Education},
0190 booktitle = {CADE-17 Workshop on Deduction Systems for Mathematics
0191 Education},
0192 OPTcrossref = {},
0193 OPTkey = {},
0194 pages = {20--25},
0195 year = {2000},
0196 editor = {E.~Melis},
0197 OPTvolume = {},
0198 OPTnumber = {},
0199 OPTseries = {},
0200 OPTaddress = {},
0201 OPTmonth = {June},
0202 OPTorganization = {},
0203 OPTpublisher = {},
0204 OPTnote = {},
0205 OPTannote = {}
0206 }
0207
0208 @Article{Farmer01,
0209 author = {W. M. Farmer},
0210 title = {{STMM}: A Set Theory for Mechanized Mathematics},
0211 journal = {Journal of Automated Reasoning},
0212 year = {2001},
0213 OPTkey = {},
0214 volume = {26},
0215 OPTnumber = {3},
0216 pages = {269--289},
0217 OPTmonth = {},
0218 OPTnote = {},
0219 OPTannote = {}
0220 }
0221
0222 @InProceedings{Farmer04,
0223 author = "W. M. Farmer",
0224 title = "Formalizing Undefinedness Arising in Calculus",
0225 booktitle = "Automated Reasoning---IJCAR 2004",
0226 year = "2004",
0227 series = "Lecture Notes in Computer Science",
0228 volume = "3097",
0229 editor = "D. Basin and M. Rusinowitch",
0230 pages = "475--489",
0231 OPTorganization = "",
0232 publisher = "Springer-Verlag",
0233 OPTaddress = "",
0234 OPTmonth = "",
0235 OPTnote = ""
0236 }
0237
0238 @TechReport{Farmer04a,
0239 author = {W. M. Farmer},
0240 title = {A Sound and Complete Proof System for
0241 {STT}{\small w}{U}},
0242 institution = {McMaster University},
0243 year = {2004},
0244 OPTkey = {},
0245 OPTtype = {},
0246 number = {No.~CAS-04-01-WF},
0247 OPTaddress = {},
0248 OPTmonth = {},
0249 OPTnote = {},
0250 OPTannote = {}
0251 }
0252
0253 @InCollection{Farmer06,
0254 author = {W. M. Farmer},
0255 title = {{IMPS}},
0256 booktitle = {The Seventeen Provers of the World},
0257 OPTcrossref = {},
0258 OPTkey = {},
0259 pages = {72--87},
0260 publisher = {Springer-Verlag},
0261 year = {2006},
0262 editor = {F. Wiedijk},
0263 volume = {3600},
0264 OPTnumber = {},
0265 series = {Lecture Notes in Computer Science},
0266 OPTtype = {},
0267 OPTchapter = {},
0268 OPTaddress = {},
0269 OPTedition = {},
0270 OPTmonth = {},
0271 OPTnote = {},
0272 OPTannote = {}
0273 }
0274
0275 @Article{FarmerGrigorov09,
0276 author = {W. M. Farmer and O. Grigorov},
0277 title = {Panoptes: An Exploration Tool for Formal Proofs},
0278 journal = {Electronic Notes in Theoretical Computer Science},
0279 year = {2009},
0280 OPTkey = {},
0281 volume = {226},
0282 OPTnumber = {},
0283 pages = {39--48},
0284 OPTmonth = {},
0285 note = {\texttt{DOI:10.1016/j.entcs.2008.12.096}},
0286 OPTannote = {}
0287 }
0288
0289 @Article{FarmerGuttman00,
0290 author = {W. M. Farmer and J. D. Guttman},
0291 title = {A Set Theory with Support for Partial Functions},
0292 journal = {Studia Logica},
0293 year = {2000},
0294 OPTkey = {},
0295 volume = {66},
0296 OPTnumber = {},
0297 pages = {59--78},
0298 OPTmonth = {},
0299 OPTnote = {},
0300 OPTannote = {}
0301 }
0302
0303 @InProceedings{FarmerMohrenschildt00,
0304 author = {W. M. Farmer and M. v. Mohrenschildt},
0305 title = {Transformers for Symbolic Computation and Formal
0306 Deduction},
0307 booktitle = {CADE-17 Workshop on the Role of Automated Deduction
0308 in Mathematics},
0309 OPTcrossref = {},
0310 OPTkey = {},
0311 pages = {36--45},
0312 year = {2000},
0313 editor = {S. Colton and U. Martin and V. Sorge},
0314 OPTvolume = {},
0315 OPTnumber = {},
0316 OPTseries = {},
0317 OPTaddress = {},
0318 OPTmonth = {June},
0319 OPTorganization = {},
0320 OPTpublisher = {},
0321 OPTnote = {},
0322 OPTannote = {}
0323 }
0324
0325 @InProceedings{FarmerEtAl90,
0326 author = "W. M. Farmer and J. D. Guttman and F. J. Thayer",
0327 title = "{IMPS}: An {I}nteractive {M}athematical {P}roof
0328 {S}ystem (system abstract)",
0329 booktitle = "10th International Conference on Automated Deduction",
0330 year = "1990",
0331 series = "Lecture Notes in Computer Science",
0332 volume = "449",
0333 editor = "M. E. Stickel",
0334 pages = "653--654",
0335 OPTorganization = "",
0336 publisher = "Springer-Verlag",
0337 OPTaddress = "",
0338 OPTmonth = "",
0339 OPTnote = ""
0340 }
0341
0342 @InProceedings{FarmerEtAl92a,
0343 author = "W. M. Farmer and J. D. Guttman and F. J. Thayer",
0344 title = "{IMPS}: System Description",
0345 booktitle = "Automated Deduction---CADE-11",
0346 year = "1992",
0347 series = "Lecture Notes in Computer Science",
0348 volume = "607",
0349 editor = "D. Kapur",
0350 pages = "701--705",
0351 OPTorganization = "",
0352 publisher = "Springer-Verlag",
0353 OPTaddress = "",
0354 OPTmonth = "",
0355 OPTnote = ""
0356 }
0357
0358 @InProceedings{FarmerEtAl92b,
0359 author = "W. M. Farmer and J. D. Guttman and F. J. Thayer",
0360 title = "Little Theories",
0361 booktitle = "Automated Deduction---CADE-11",
0362 year = "1992",
0363 series = "Lecture Notes in Computer Science",
0364 volume = "607",
0365 editor = "D. Kapur",
0366 pages = "567--581",
0367 OPTorganization = "",
0368 publisher = "Springer-Verlag",
0369 OPTaddress = "",
0370 OPTmonth = "",
0371 OPTnote = ""
0372 }
0373
0374 @Article{FarmerEtAl93,
0375 author = "W. M. Farmer and J. D. Guttman and F. J. Thayer",
0376 title = "{IMPS}: An {I}nteractive {M}athematical {P}roof {S}ystem",
0377 journal = "Journal of Automated Reasoning",
0378 year = "1993",
0379 volume = "11",
0380 OPTnumber = "2",
0381 pages = "213--248",
0382 OPTmonth = "October"
0383 }
0384
0385 @InProceedings{FarmerEtAl93a,
0386 author = "W. M. Farmer and J. D. Guttman and F. J. Thayer",
0387 title = "Reasoning with Contexts",
0388 booktitle = "Design and Implementation of Symbolic Computation Systems",
0389 year = "1993",
0390 series = "Lecture Notes in Computer Science",
0391 volume = "722",
0392 editor = "A. Miola",
0393 pages = "216--228",
0394 OPTorganization = "",
0395 publisher = "Springer-Verlag",
0396 OPTaddress = "",
0397 OPTmonth = "",
0398 OPTnote = ""
0399 }
0400
0401 @TechReport{FarmerEtAl93b,
0402 author = "W. M. Farmer and J. D. Guttman and F. J. Thayer",
0403 title = "The {IMPS} User's Manual",
0404 institution = "The {MITRE} Corporation",
0405 year = "1993",
0406 OPTtype = "",
0407 number = "M-93B138",
0408 OPTaddress = "202 Burlington Road, Bedford, MA 01730-1420, USA",
0409 OPTmonth = "November",
0410 OPTnote = "Available at
0411 \url{ftp://math.harvard.edu/imps/doc/}"
0412 }
0413
0414 @InProceedings{FarmerEtAl94,
0415 author = "W. M. Farmer and J. D. Guttman and M. E. Nadel and
0416 F. J. Thayer",
0417 title = "Proof Script Pragmatics in {IMPS}",
0418 booktitle = "Automated Deduction---CADE-12",
0419 year = "1994",
0420 series = "Lecture Notes in Computer Science",
0421 volume = "814",
0422 editor = "A. Bundy",
0423 pages = "356--370",
0424 OPTorganization = "",
0425 publisher = "Springer-Verlag",
0426 OPTaddress = "",
0427 OPTmonth = "",
0428 OPTnote = ""
0429 }
0430
0431 @Article{FarmerEtAl95,
0432 author = "W. M. Farmer and J. D. Guttman and F. J. Thayer",
0433 title = "Contexts in Mathematical Reasoning and Computation",
0434 OPTcrossref = "",
0435 OPTkey = "",
0436 journal = "Journal of Symbolic Computation",
0437 year = "1995",
0438 volume = "19",
0439 OPTnumber = "",
0440 pages = "201--216",
0441 OPTmonth = "",
0442 OPTnote = "",
0443 OPTannote = "",
0444 patron = "Farmer"
0445 }
0446
0447 @InProceedings{FarmerEtAl96,
0448 author = "W. M. Farmer and J. D. Guttman and F. J. {Thayer F\'abrega}",
0449 title = "{IMPS}: An Updated System Description",
0450 booktitle = "Automated Deduction---CADE-13",
0451 year = "1996",
0452 series = "Lecture Notes in Computer Science",
0453 volume = "1104",
0454 editor = "M. McRobbie and J. Slaney",
0455 pages = "298--302",
0456 OPTorganization = "",
0457 publisher = "Springer-Verlag",
0458 OPTaddress = "",
0459 OPTmonth = "",
0460 OPTnote = ""
0461 }
0462
0463 @Article{FarmerThayer91,
0464 author = "W. M. Farmer and F. J. Thayer",
0465 title = "Two Computer-Supported Proofs in Metric Space Topology",
0466 journal = "Notices of the American Mathematical Society",
0467 year = "1991",
0468 volume = "38",
0469 OPTnumber = "9",
0470 pages = "1133--1138",
0471 OPTmonth = "",
0472 OPTnote = ""
0473 }
0474
0475 @TechReport{FarmerThayer94,
0476 author = "W. M. Farmer and F. J. Thayer",
0477 title = "Formal Numerical Program Analysis",
0478 institution = "The {MITRE} Corporation",
0479 year = "1994",
0480 OPTtype = "",
0481 OPTnumber = "",
0482 OPTaddress = "202 Burlington Road, Bedford, MA 01730-1420, USA",
0483 OPTmonth = "",
0484 OPTnote = ""
0485 }
0486
0487 @TechReport{Guttman91,
0488 author = "J. D. Guttman",
0489 title = "A Proposed Interface Logic for Verification Environments",
0490 institution = "The {MITRE} Corporation",
0491 year = "1991",
0492 OPTtype = "",
0493 number = "M91-19",
0494 OPTaddress = "202 Burlington Road, Bedford, MA 01730-1420, USA",
0495 OPTmonth = "",
0496 OPTnote = ""
0497 }
0498
0499 @InProceedings{Guttman92,
0500 author = "J. D. Guttman",
0501 title = "Building Verification Environments from Components:
0502 A Position Paper",
0503 booktitle = "Proceedings, Workshop on Effective Use of Automated
0504 Reasoning Technology in System Development",
0505 year = "1992",
0506 OPTeditor = "",
0507 pages = "4--17",
0508 OPTorganization = "",
0509 OPTpublisher = "",
0510 address = "Naval Research Laboratory, Washington, D.C.",
0511 month = "April",
0512 OPTnote = ""
0513 }
0514
0515 @TechReport{Guttman94,
0516 author = "J. D. Guttman",
0517 title = "A Simple Virtual Memory Scheme Formalized in {IMPS}",
0518 institution = "The {MITRE} Corporation",
0519 year = "1994",
0520 patron = "Guttman"
0521 }
0522
0523 @InCollection{GuttmanJohnson94,
0524 author = "J. D. Guttman and D. M. Johnson",
0525 title = "Three Applications of {Formal} {Methods} at {MITRE}",
0526 booktitle = "FME '94: Industrial Benefits of Formal Methods",
0527 publisher = "Springer Verlag",
0528 year = 1994,
0529 editor = "M. Naftalin and T. Denvir and M. Bertran",
0530 volume = 873,
0531 series = "Lecture Notes in Computer Science",
0532 pages = "55--65",
0533 patron = "Guttman"
0534 }
0535
0536 @TechReport{Monk86,
0537 author = "L. G. Monk",
0538 title = "{PDLM}: A {P}roof {D}evelopment {L}anguage for
0539 {M}athematics",
0540 institution = "The {MITRE} Corporation",
0541 year = "1986",
0542 OPTtype = "",
0543 number = "M86-37",
0544 OPTaddress = "202 Burlington Road, Bedford, MA 01730-1420, USA",
0545 OPTmonth = "",
0546 OPTnote = ""
0547 }
0548
0549 @Article{Monk88,
0550 author = "L. G. Monk",
0551 title = "Inference Rules Using Local Contexts",
0552 journal = "Journal of Automated Reasoning",
0553 year = "1988",
0554 volume = "4",
0555 OPTnumber = "4",
0556 pages = "445--462",
0557 OPTmonth = "",
0558 OPTnote = ""
0559 }
0560
0561 @Manual{ReesEtAl90,
0562 title = "The T Manual",
0563 author = "J. A. Rees and N. I. Adams and J. R. Meehan",
0564 organization = "Computer Science Department, Yale University",
0565 OPTaddress = "",
0566 edition = "Fifth",
0567 year = "1990",
0568 OPTmonth = "",
0569 OPTnote = ""
0570 }
0571
0572 @TechReport{Thayer87,
0573 author = "F. J. Thayer",
0574 title = "Obligated Term Replacements",
0575 institution = "The {MITRE} Corporation",
0576 year = "1987",
0577 OPTtype = "",
0578 number = "MTR-10301",
0579 OPTaddress = "202 Burlington Road, Bedford, MA 01730-1420, USA",
0580 OPTmonth = "",
0581 OPTnote = ""
0582 }
0583
0584 @TechReport{Thayer94,
0585 author = "F. J. Thayer",
0586 title = "An Approach to Process Algebra using {IMPS}",
0587 institution = "The {MITRE} Corporation",
0588 year = "1994",
0589 OPTtype = "",
0590 number = "MP-94B193",
0591 OPTaddress = "202 Burlington Road, Bedford, MA 01730-1420, USA",
0592 OPTmonth = "",
0593 OPTnote = ""
0594 }
0595
0596 @TechReport{ThayerGuttman95,
0597 author = "F. J. Thayer and J. D. Guttman",
0598 title = "Copy on Write",
0599 institution = "The {MITRE} Corporation",
0600 year = "1995",
0601 OPTcrossref = "",
0602 OPTkey = "",
0603 OPTtype = "",
0604 OPTnumber = "",
0605 OPTaddress = "202 Burlington Road, Bedford, MA 01730-1420, USA",
0606 OPTmonth = "",
0607 OPTnote = "",
0608 OPTannote = ""
0609 }
0610
0611 @MastersThesis{Miller02,
0612 author = {D. Miller},
0613 title = {Two Formal Theories of Character Strings},
0614 school = {McMaster University},
0615 year = {2002},
0616 OPTkey = {},
0617 OPTtype = {},
0618 OPTaddress = {Hamilton, Ontario, Canada},
0619 OPTmonth = {},
0620 OPTnote = {},
0621 OPTannote = {}
0622 }
0623
0624 @MastersThesis{Tan02,
0625 author = {P. Tan},
0626 title = {Mechanical Verification of Machine Integer Programs
0627 in a Fragment of {C}},
0628 school = {McMaster University},
0629 year = {2002},
0630 OPTkey = {},
0631 OPTtype = {},
0632 OPTaddress = {Hamilton, Ontario, Canada},
0633 OPTmonth = {},
0634 OPTnote = {},
0635 OPTannote = {}
0636 }
0637
0638 @MastersThesis{Li02,
0639 author = {Y. Li},
0640 title = {{IMPS} to {OMDoc} Translation},
0641 school = {McMaster University},
0642 year = {2002},
0643 OPTkey = {},
0644 OPTtype = {},
0645 OPTaddress = {Hamilton, Ontario, Canada},
0646 OPTmonth = {},
0647 OPTnote = {},
0648 OPTannote = {}
0649 }
0650
0651 @MastersThesis{Grigorov08,
0652 author = {O. Grigorov},
0653 title = {Panoptes: An Exploration Tool for Formal Proofs},
0654 school = {McMaster University},
0655 year = {2008},
0656 OPTkey = {},
0657 OPTtype = {},
0658 OPTaddress = {Hamilton, Ontario, Canada},
0659 OPTmonth = {},
0660 OPTnote = {},
0661 OPTannote = {}
0662 }