%% 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 = {}
}