%% This file is a complete bibliography of the papers on IMPS in 
%% BibTeX format.  Send questions to wmfarmer at mcmaster.ca.

@TechReport{Farmer87,
  author = 	"W. M. Farmer",
  title = 	"Abstract Data Types in Many-Sorted Second-Order Logic",
  institution = "The {MITRE} Corporation",
  year = 	"1987",
  OPTtype = 	"",
  number = 	"M87-64",
  OPTaddress = 	"202 Burlington Road, Bedford, MA 01730-1420, USA",
  OPTmonth = 	"",
  OPTnote = 	""
}

@Article{Farmer90,
  author = 	"W. M. Farmer",
  title = 	"A Partial Functions Version of {Church's} Simple 
                 Theory of Types",
  journal = 	"Journal of Symbolic Logic",
  year = 	"1990",
  volume = 	"55",
  Optnumber = 	"3",
  pages = 	"1269--91",
  OPTmonth = 	"",
  OPTnote = 	"Also {MITRE} Corporation technical report M88-52,
		 1988; revised 1990."
}

@Article{Farmer93b,
  author = 	"W. M. Farmer",
  title = 	"A Simple Type Theory with Partial Functions and Subtypes",
  journal = 	"Annals of Pure and Applied Logic",
  year = 	"1993",
  volume = 	"64",
  OPTnumber = 	"3",
  pages = 	"211--240",
  OPTmonth = 	"",
  OPTnote = 	""
}

@InProceedings{Farmer94,
  author = 	"W. M. Farmer",
  title = 	"Theory Interpretation in Simple Type Theory",
  booktitle =   "Higher-Order Algebra, Logic, and Term Rewriting",
  year = 	"1994",
  series =      "Lecture Notes in Computer Science",
  volume =      "816",
  editor = 	"J. Heering et al.",
  pages = 	"96--123",
  publisher = 	"Springer-Verlag",
  OPTnote =     ""
}

@TechReport{Farmer94a,
  author = 	"W. M. Farmer",
  title = 	"A General Method for Safely Overwriting Theories in
		 Mechanized Mathematics Systems",
  institution = "The {MITRE} Corporation",
  year = 	"1994",
  OPTtype = 	"",
  OPTnumber = 	"",
  OPTaddress = 	"202 Burlington Road, Bedford, MA 01730-1420, USA",
  OPTmonth = 	"",
  OPTnote = 	"Revised version of the technical report ``A
		 technique for safely extending axiomatic theories''."
}

@Article{Farmer95,
  author = 	 "W. M. Farmer",
  title = 	 "Reasoning about Partial Functions with the Aid of a
		  Computer",
  OPTcrossref =  "",
  OPTkey = 	 "",
  journal = 	 "Erkenntnis",
  year = 	 "1995",
  volume = 	 "43",
  OPTnumber = 	 "3",
  pages = 	 "279--294",
  OPTmonth = 	 "",
  OPTnote = 	 "",
  OPTannote = 	 "",
  patron =       "Farmer"
}

@InProceedings{Farmer96,
  author = 	 {W. M. Farmer},
  title = 	 {Mechanizing the Traditional Approach to Partial Functions},
  booktitle = 	 {CADE-13 Workshop on the Mechanization of 
                 Partial Functions},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages = 	 {27--32},
  year = 	 {1996},
  editor = 	 {W.~Farmer and M.~Kerber and M.~Kohlhase},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {July},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{Farmer98,
  author = 	 {W. M. Farmer},
  title = 	 {{STMM} and Partial Functions},
  booktitle = 	 {CADE-15 Workshop on the Mechanization of 
                 Partial Functions},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages = 	 {3--14},
  year = 	 {1998},
  editor = 	 {M.~Kerber},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {July},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{Farmer98a,
  author = 	 {W. M. Farmer},
  title = 	 {The Interactive Mathematics Laboratory},
  booktitle = 	 {Proceedings of the 31st Annual Midwest Instruction 
                  and Computing Symposium (MICS '98)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages = 	 {16--18},
  year = 	 {1998},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month = 	 {April},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{Farmer99,
  author = 	 {W. M. Farmer},
  title = 	 {A Scheme for Defining Partial Higher-Order
                  Functions by Recursion},
  booktitle = 	 {3rd Irish Workshop on Formal Methods},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  year = 	 {1999},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  series = 	 {electronic Workshops in Computing, \urlpart{http://}\urlpart{ewic.org.uk/}\urlpart{workshops}},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{Farmer00,
  author = 	"W. M. Farmer",
  title = 	"An Infrastructure for Intertheory Reasoning",
  booktitle = 	"Automated Deduction---CADE-17",
  year = 	"2000",
  series =      "Lecture Notes in Computer Science",
  volume =      "1831",
  editor = 	"D. McAllester",
  pages = 	"115--131",
  OPTorganization = 	"",
  publisher = 	"Springer-Verlag",
  OPTaddress = 	"",
  OPTmonth = 	"",
  OPTnote = 	""
}

@InProceedings{Farmer00a,
  author = 	 {W. M. Farmer},
  title = 	 {A Proposal for the Development of an Interactive
                  Mathematics Laboratory for Mathematics Education},
  booktitle = 	 {CADE-17 Workshop on Deduction Systems for Mathematics 
                  Education},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages = 	 {20--25},
  year = 	 {2000},
  editor = 	 {E.~Melis},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {June},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{Farmer01,
  author = 	 {W. M. Farmer},
  title = 	 {{STMM}: A Set Theory for Mechanized Mathematics},
  journal = 	 {Journal of Automated Reasoning},
  year = 	 {2001},
  OPTkey = 	 {},
  volume = 	 {26},
  OPTnumber = 	 {3},
  pages = 	 {269--289},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{Farmer04,
  author = 	"W. M. Farmer",
  title = 	"Formalizing Undefinedness Arising in Calculus",
  booktitle = 	"Automated Reasoning---IJCAR 2004",
  year = 	"2004",
  series =      "Lecture Notes in Computer Science",
  volume =      "3097",
  editor = 	"D. Basin and M. Rusinowitch",
  pages = 	"475--489",
  OPTorganization = 	"",
  publisher = 	"Springer-Verlag",
  OPTaddress = 	"",
  OPTmonth = 	"",
  OPTnote = 	""
}

@TechReport{Farmer04a,
  author = 	 {W. M. Farmer},
  title = 	 {A Sound and Complete Proof System for 
                  {STT}{\small w}{U}},
  institution =  {McMaster University},
  year = 	 {2004},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number = 	 {No.~CAS-04-01-WF},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InCollection{Farmer06,
  author = 	 {W. M. Farmer},
  title = 	 {{IMPS}},
  booktitle = 	 {The Seventeen Provers of the World},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages = 	 {72--87},
  publisher =    {Springer-Verlag},
  year = 	 {2006},
  editor = 	 {F. Wiedijk},
  volume = 	 {3600},
  OPTnumber = 	 {},
  series = 	 {Lecture Notes in Computer Science},
  OPTtype = 	 {},
  OPTchapter = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{FarmerGrigorov09,
  author = 	 {W. M. Farmer and O. Grigorov},
  title = 	 {Panoptes: An Exploration Tool for Formal Proofs},
  journal = 	 {Electronic Notes in Theoretical Computer Science},
  year = 	 {2009},
  OPTkey = 	 {},
  volume = 	 {226},
  OPTnumber = 	 {},
  pages = 	 {39--48},
  OPTmonth = 	 {},
  note = 	 {\texttt{DOI:10.1016/j.entcs.2008.12.096}},
  OPTannote = 	 {}
}

@Article{FarmerGuttman00,
  author = 	 {W. M. Farmer and J. D. Guttman},
  title = 	 {A Set Theory with Support for Partial Functions},
  journal = 	 {Studia Logica},
  year = 	 {2000},
  OPTkey = 	 {},
  volume = 	 {66},
  OPTnumber = 	 {},
  pages = 	 {59--78},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{FarmerMohrenschildt00,
  author = 	 {W. M. Farmer and M. v. Mohrenschildt},
  title = 	 {Transformers for Symbolic Computation and Formal
                  Deduction},
  booktitle = 	 {CADE-17 Workshop on the Role of Automated Deduction 
                  in Mathematics},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages = 	 {36--45},
  year = 	 {2000},
  editor = 	 {S. Colton and U. Martin and V. Sorge},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {June},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{FarmerEtAl90,
  author = 	"W. M. Farmer and J. D. Guttman and F. J. Thayer",
  title = 	"{IMPS}: An {I}nteractive {M}athematical {P}roof 
                 {S}ystem (system abstract)",
  booktitle = 	"10th International Conference on Automated Deduction",
  year = 	"1990",
  series =      "Lecture Notes in Computer Science",
  volume =      "449",
  editor = 	"M. E. Stickel",
  pages = 	"653--654",
  OPTorganization = 	"",
  publisher = 	"Springer-Verlag",
  OPTaddress = 	"",
  OPTmonth = 	"",
  OPTnote = 	""
}

@InProceedings{FarmerEtAl92a,
  author = 	"W. M. Farmer and J. D. Guttman and F. J. Thayer",
  title = 	"{IMPS}: System Description",
  booktitle = 	"Automated Deduction---CADE-11",
  year = 	"1992",
  series =      "Lecture Notes in Computer Science",
  volume =      "607",
  editor = 	"D. Kapur",
  pages = 	"701--705",
  OPTorganization = 	"",
  publisher = 	"Springer-Verlag",
  OPTaddress = 	"",
  OPTmonth = 	"",
  OPTnote = 	""
}

@InProceedings{FarmerEtAl92b,
  author = 	"W. M. Farmer and J. D. Guttman and F. J. Thayer",
  title = 	"Little Theories",
  booktitle = 	"Automated Deduction---CADE-11",
  year = 	"1992",
  series =      "Lecture Notes in Computer Science",
  volume =      "607",
  editor = 	"D. Kapur",
  pages = 	"567--581",
  OPTorganization = 	"",
  publisher = 	"Springer-Verlag",
  OPTaddress = 	"",
  OPTmonth = 	"",
  OPTnote = 	""
}

@Article{FarmerEtAl93,
  author = 	"W. M. Farmer and J. D. Guttman and F. J. Thayer",
  title = 	"{IMPS}: An {I}nteractive {M}athematical {P}roof {S}ystem",
  journal = 	"Journal of Automated Reasoning",
  year = 	"1993",
  volume = 	"11",
  OPTnumber = 	"2",
  pages = 	"213--248",
  OPTmonth = 	"October"
}

@InProceedings{FarmerEtAl93a,
  author = 	"W. M. Farmer and J. D. Guttman and F. J. Thayer",
  title = 	"Reasoning with Contexts",
  booktitle = 	"Design and Implementation of Symbolic Computation Systems",
  year = 	"1993",
  series =      "Lecture Notes in Computer Science",
  volume =      "722",
  editor = 	"A. Miola",
  pages = 	"216--228",
  OPTorganization = 	"",
  publisher = 	"Springer-Verlag",
  OPTaddress = 	"",
  OPTmonth = 	"",
  OPTnote = 	""
}

@TechReport{FarmerEtAl93b,
  author = 	"W. M. Farmer and J. D. Guttman and F. J. Thayer",
  title = 	"The {IMPS} User's Manual",
  institution = "The {MITRE} Corporation",
  year = 	"1993",
  OPTtype = 	"",
  number = 	"M-93B138",
  OPTaddress = 	"202 Burlington Road, Bedford, MA 01730-1420, USA",
  OPTmonth = 	"November",
  OPTnote = 	"Available at 
                 \urlpart{ftp://math.harvard.edu/}\urlpart{imps/}\urlpart{doc/}"
}

@InProceedings{FarmerEtAl94,
  author = 	"W. M. Farmer and J. D. Guttman and M. E. Nadel and 
                 F. J. Thayer",
  title = 	"Proof Script Pragmatics in {IMPS}",
  booktitle = 	"Automated Deduction---CADE-12",
  year = 	"1994",
  series =      "Lecture Notes in Computer Science",
  volume =      "814",
  editor = 	"A. Bundy",
  pages = 	"356--370",
  OPTorganization = 	"",
  publisher = 	"Springer-Verlag",
  OPTaddress = 	"",
  OPTmonth = 	"",
  OPTnote = 	""
}

@Article{FarmerEtAl95,
  author = 	 "W. M. Farmer and J. D. Guttman and F. J. Thayer",
  title = 	 "Contexts in Mathematical Reasoning and Computation",
  OPTcrossref =  "",
  OPTkey = 	 "",
  journal = 	 "Journal of Symbolic Computation",
  year = 	 "1995",
  volume = 	 "19",
  OPTnumber = 	 "",
  pages = 	 "201--216",
  OPTmonth = 	 "",
  OPTnote = 	 "",
  OPTannote = 	 "",
  patron =       "Farmer"
}

@InProceedings{FarmerEtAl96,
  author = 	"W. M. Farmer and J. D. Guttman and F. J. {Thayer F\'abrega}",
  title = 	"{IMPS}: An Updated System Description",
  booktitle = 	"Automated Deduction---CADE-13",
  year = 	"1996",
  series =      "Lecture Notes in Computer Science",
  volume =      "1104",
  editor = 	"M. McRobbie and J. Slaney",
  pages = 	"298--302",
  OPTorganization = 	"",
  publisher = 	"Springer-Verlag",
  OPTaddress = 	"",
  OPTmonth = 	"",
  OPTnote = 	""
}

@Article{FarmerThayer91,
  author = 	"W. M. Farmer and F. J. Thayer",
  title = 	"Two Computer-Supported Proofs in Metric Space Topology",
  journal = 	"Notices of the American Mathematical Society",
  year = 	"1991",
  volume = 	"38",
  OPTnumber = 	"9",
  pages = 	"1133--1138",
  OPTmonth = 	"",
  OPTnote = 	""
}

@TechReport{FarmerThayer94,
  author = 	"W. M. Farmer and F. J. Thayer",
  title = 	"Formal Numerical Program Analysis",
  institution = "The {MITRE} Corporation",
  year = 	"1994",
  OPTtype = 	"",
  OPTnumber = 	"",
  OPTaddress = 	"202 Burlington Road, Bedford, MA 01730-1420, USA",
  OPTmonth = 	"",
  OPTnote = 	""
}

@TechReport{Guttman91,
  author = 	"J. D. Guttman",
  title = 	"A Proposed Interface Logic for Verification Environments",
  institution = "The {MITRE} Corporation",
  year = 	"1991",
  OPTtype = 	"",
  number = 	"M91-19",
  OPTaddress = 	"202 Burlington Road, Bedford, MA 01730-1420, USA",
  OPTmonth = 	"",
  OPTnote = 	""
}

@InProceedings{Guttman92,
  author = 	"J. D. Guttman",
  title = 	"Building Verification Environments from Components: 
                 A Position Paper",
  booktitle = 	"Proceedings, Workshop on Effective Use of Automated 
                 Reasoning Technology in System Development",
  year = 	"1992",
  OPTeditor = 	"",
  pages = 	"4--17",
  OPTorganization = 	"",
  OPTpublisher = 	"",
  address = 	"Naval Research Laboratory, Washington, D.C.",
  month = 	"April",
  OPTnote = 	""
}

@TechReport{Guttman94,
  author = 	 "J. D. Guttman",
  title = 	 "A Simple Virtual Memory Scheme Formalized in {IMPS}",
  institution =  "The {MITRE} Corporation",
  year = 	 "1994",
  patron =	"Guttman"
}

@InCollection{GuttmanJohnson94,
  author = 	 "J. D. Guttman and D. M. Johnson",
  title = 	 "Three Applications of {Formal} {Methods} at {MITRE}",
  booktitle =	 "FME '94:  Industrial Benefits of Formal Methods",
  publisher =	 "Springer Verlag",
  year = 	 1994,
  editor = 	 "M. Naftalin and T. Denvir and M. Bertran",
  volume = 	 873,
  series = 	 "Lecture Notes in Computer Science",
  pages = 	 "55--65",
  patron =	"Guttman"
}

@TechReport{Monk86,
  author = 	"L. G. Monk",
  title = 	"{PDLM}: A {P}roof {D}evelopment {L}anguage for 
                 {M}athematics",
  institution = "The {MITRE} Corporation",
  year = 	"1986",
  OPTtype = 	"",
  number = 	"M86-37",
  OPTaddress = 	"202 Burlington Road, Bedford, MA 01730-1420, USA",
  OPTmonth = 	"",
  OPTnote = 	""
}

@Article{Monk88,
  author = 	"L. G. Monk",
  title = 	"Inference Rules Using Local Contexts",
  journal = 	"Journal of Automated Reasoning",
  year = 	"1988",
  volume = 	"4",
  OPTnumber = 	"4",
  pages = 	"445--462",
  OPTmonth = 	"",
  OPTnote = 	""
}

@Manual{ReesEtAl90,
  title = 	"The T Manual",
  author = 	"J. A. Rees and N. I. Adams and J. R. Meehan",
  organization = 	"Computer Science Department, Yale University",
  OPTaddress = 	"",
  edition = 	"Fifth",
  year = 	"1990",
  OPTmonth = 	"",
  OPTnote = 	""
}

@TechReport{Thayer87,
  author = 	"F. J. Thayer",
  title = 	"Obligated Term Replacements",
  institution = "The {MITRE} Corporation",
  year = 	"1987",
  OPTtype = 	"",
  number = 	"MTR-10301",
  OPTaddress = 	"202 Burlington Road, Bedford, MA 01730-1420, USA",
  OPTmonth = 	"",
  OPTnote = 	""
}

@TechReport{Thayer94,
  author = 	"F. J. Thayer",
  title = 	"An Approach to Process Algebra using {IMPS}",
  institution = "The {MITRE} Corporation",
  year = 	"1994",
  OPTtype = 	"",
  number = 	"MP-94B193",
  OPTaddress = 	"202 Burlington Road, Bedford, MA 01730-1420, USA",
  OPTmonth = 	"",
  OPTnote = 	""
}

@TechReport{ThayerGuttman95,
  author = 	 "F. J. Thayer and J. D. Guttman",
  title = 	 "Copy on Write",
  institution =  "The {MITRE} Corporation",
  year = 	 "1995",
  OPTcrossref =  "",
  OPTkey = 	 "",
  OPTtype = 	 "",
  OPTnumber = 	 "",
  OPTaddress = 	 "202 Burlington Road, Bedford, MA 01730-1420, USA",
  OPTmonth = 	 "",
  OPTnote = 	 "",
  OPTannote = 	 ""
}

@MastersThesis{Miller02,
  author = 	 {D. Miller},
  title = 	 {Two Formal Theories of Character Strings},
  school = 	 {McMaster University},
  year = 	 {2002},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {Hamilton, Ontario, Canada},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@MastersThesis{Tan02,
  author = 	 {P. Tan},
  title = 	 {Mechanical Verification of Machine Integer Programs 
                  in a Fragment of {C}},
  school = 	 {McMaster University},
  year = 	 {2002},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {Hamilton, Ontario, Canada},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@MastersThesis{Li02,
  author = 	 {Y. Li},
  title = 	 {{IMPS} to {OMDoc} Translation},
  school = 	 {McMaster University},
  year = 	 {2002},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {Hamilton, Ontario, Canada},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@MastersThesis{Grigorov08,
  author = 	 {O. Grigorov},
  title = 	 {Panoptes: An Exploration Tool for Formal Proofs},
  school = 	 {McMaster University},
  year = 	 {2008},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {Hamilton, Ontario, Canada},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}