@inproceedings(conf/tacas/Aspinall00,
 author       = "David Aspinall",
 year         = "2000",
 title        = "Proof General: {A} Generic Tool for Proof Development",
 editor       = "Susanne Graf and Michael I. Schwartzbach",
 booktitle    = "TACAS",
 series       = "LNCS",
 volume       = "1785",
 publisher    = "Springer",
 pages        = "38--42",
 url          = "http://dx.doi.org/10.1007/3-540-46419-0_3",
)
@inproceedings(conf/cade/Autexier05,
 author       = "Serge Autexier",
 year         = "2005",
 title        = "The CoRe Calculus",
 editor       = "Robert Nieuwenhuis",
 booktitle    = "Automated Deduction - {CADE}-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "3632",
 publisher    = "Springer",
 pages        = "84--98",
 url          = "http://dx.doi.org/10.1007/11532231_7",
)
@article(journals/eik/Basin94,
 author       = "David A. Basin",
 year         = "1994",
 title        = "Generalized Rewriting in Type Theory",
 journal      = "Elektronische Informationsverarbeitung und Kybernetik",
 volume       = "30",
 number       = "5/6",
 pages        = "249--259",
 url          = "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.3314",
)
@book(bk:Coq'Art:04,
 author       = "Yves Bertot and P. (Pierre) Cast{\'e}ran",
 year         = "2004",
 title        = "Interactive theorem proving and program development: {Coq'Art}: the calculus of inductive constructions",
 series       = "Texts in theoretical computer science",
 publisher    = "Springer Verlag",
 doi          = "10.1007/978-3-662-07964-5",
)
@inproceedings(conf/tacs/BertotKT94,
 author       = "Yves Bertot and Gilles Kahn and Laurent Th{\'e}ry",
 year         = "1994",
 title        = "Proof by Pointing",
 editor       = "Masami Hagiya and John C. Mitchell",
 booktitle    = "Theoretical Aspects of Computer Software, International Conference {TACS} '94, Sendai, Japan, April 19-22, 1994, Proceedings",
 series       = "LNCS",
 volume       = "789",
 publisher    = "Springer",
 pages        = "141--160",
 url          = "http://dx.doi.org/10.1007/3-540-57887-0_94",
)
@inproceedings(conf/utp/Butterfield10,
 author       = "Andrew Butterfield",
 year         = "2010",
 title        = "Saoithin: A Theorem Prover for UTP",
 editor       = "Shenchao Qin",
 booktitle    = "Unifying Theories of Programming, Third International Symposium, UTP 2010, Shanghai, China, November, 2010.",
 series       = "LNCS",
 volume       = "6445",
 publisher    = "Springer",
 address      = "Shanghai, China",
 pages        = "137--156",
 url          = "http://dx.doi.org/10.1007/978-3-642-16690-7_6",
)
@inproceedings(conf/utp/Butterfield12,
 author       = "Andrew Butterfield",
 year         = "2012",
 title        = "The Logic of {$U\mskip -\thinmuskip \cdot \mskip -\thinmuskip (TP)^2$}",
 pages        = "124--143",
 url          = "http://dx.doi.org/10.1007/978-3-642-35705-3_6",
)
@inproceedings(conf/vstte/FeliachiGW12,
 author       = "Abderrahmane Feliachi and Marie-Claude Gaudel and Burkhart Wolff",
 year         = "2012",
 title        = "Isabelle/Circus: {A} Process Specification and Verification Environment",
 editor       = "Rajeev Joshi and Peter M{\"u}ller and Andreas Podelski",
 booktitle    = "Verified Software: Theories, Tools, Experiments - 4th International Conference, {VSTTE} 2012, Philadelphia, {PA}, {USA}, January 28-29, 2012. Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "7152",
 publisher    = "Springer",
 pages        = "243--260",
 url          = "http://dx.doi.org/10.1007/978-3-642-27705-4_20",
)
@inproceedings(conf/utp/FZW14,
 author       = "Simon Foster and Frank Zeyda and Jim Woodcock",
 year         = "to appear",
 title        = "{Isabelle/UTP}: A mechanised theory engineering framework",
 editor       = "David Naumann",
 booktitle    = "Unifying Theories of Programming, Fifth International Symposium, {UTP} 2014, National University of Singapore, May 13, 2014,",
)
@book(gries.93,
 author       = "David Gries and Fred B. Schneider",
 year         = "1993",
 title        = "A Logical Approach to Discrete Math",
 series       = "Texts and Monographs in Computer Science",
 publisher    = "Berlin: Springer Verlag",
 doi          = "10.1007/978-1-4757-3837-7",
)
@article(predprog,
 author       = "Eric C. R. Hehner",
 year         = "1984",
 title        = "Predicative programming --- {P}art {I}\tmspace +\thinmuskip {.1667em}\&\tmspace +\thinmuskip {.1667em}{II}",
 journal      = "Commun. ACM",
 volume       = "27",
 number       = "2",
 pages        = "134--151",
 doi          = "10.1145/69610.357990",
)
@book(UTP-book,
 author       = "C. A. R. Hoare and Jifeng He",
 year         = "1998",
 title        = "Unifying Theories of Programming",
 publisher    = "Prentice-Hall",
)
@inproceedings(Hutter96,
 author       = "Dieter Hutter and Claus Sengler",
 year         = "1996",
 title        = "The Graphical User Interface of INKA",
 editor       = "Nicholas A. Merriam",
 booktitle    = "Proceedings International Workshop on User Interfaces for Theorem Provers",
 publisher    = "N. Merriam",
 pages        = "43--50",
 url          = "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.9511",
)
@book(books/sp/NipkowPW02,
 author       = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
 year         = "2002",
 title        = "Isabelle/{HOL} - {A} Proof Assistant for Higher-Order Logic",
 series       = "Lecture Notes in Computer Science",
 volume       = "2283",
 publisher    = "Springer",
 url          = "http://www.springer.com/computer/theoretical+computer+science/book/978-3-540-43376-7",
)
@inproceedings(conf/fmcad/Shankar96,
 author       = "Natarajan Shankar",
 year         = "1996",
 title        = "{PVS}: Combining Specification, Proof Checking, and Model Checking",
 editor       = "Mandayam K. Srivas and Albert John Camilleri",
 booktitle    = "Formal Methods in Computer-Aided Design, First International Conference, {FMCAD} '96",
 series       = "LNCS",
 volume       = "1166",
 publisher    = "Springer",
 pages        = "257--264",
 doi          = "10.1007/BFb0031813",
)
@misc(oai:CiteSeerXPSU:10.1.1.42.1864,
 author       = "J{\"o}rg Siekmann and Stephan Hess and Christoph Benzm{\"u}ller and Lassaad Cheikhrouhou and Armin Fiedler and Helmut Horacek and Michael Kohlhase and Karsten Konrad and Andreas Meier and Erica Melis and Martin Pollet and Volker Sorge",
 year         = "1999",
 title        = "{LO}mega{UI}: Lovely {OMEGA} User Interface",
 url          = "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.1864",
)
@misc(Staples95,
 author       = "Mark Staples",
 year         = "1995",
 title        = "Window Inference in Isabelle",
 url          = "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.6012",
)
@article(journals/logcom/Tourlakis01,
 author       = "George Tourlakis",
 year         = "2001",
 title        = "On the Soundness and Completeness of Equational Predicate Logics",
 journal      = "J. Log. Comput.",
 volume       = "11",
 number       = "4",
 pages        = "623--653",
 doi          = "10.1093/logcom/11.4.623",
 url          = "http://www3.oup.co.uk/logcom/hdb/Volume_11/Issue_04/110623.sgm.abs.html",
)
@proceedings(conf/tphol/2006provers,
 editor       = "Freek Wiedijk",
 year         = "2006",
 title        = "The Seventeen Provers of the World, Foreword by Dana {S}. Scott",
 series       = "Lecture Notes in Computer Science",
 volume       = "3600",
 publisher    = "Springer",
 url          = "http://www.springer.com/computer/ai/book/978-3-540-30704-4",
)
@inproceedings(conf/utp/ZC08,
 author       = "Frank Zeyda and Ana Cavalcanti",
 year         = "2008",
 title        = "Encoding {\textit {Circus}} Programs in {ProofPower-Z}",
 editor       = "Andrew Butterfield",
 booktitle    = "Unifying Theories of Programming, Second International Symposium, {UTP} 2008, Trinity College, Dublin, {Ireland}, September 8-10, 2008, Revised Selected Papers",
 series       = "Lecture Notes in Computer Science",
 volume       = "5713",
 publisher    = "Springer",
 pages        = "218--237",
 doi          = "10.1007/978-3-642-14521-6\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}13",
)