@phdthesis{Grov09,
	Author = {Gudmund Grov},
	Month = {March},
	School = {Heriot-Watt University},
	Title = {{R}easoning about {C}orrectness {P}roperties of a {C}oordination {P}rogramming {L}anguage},
	Year = {2009}}

@inproceedings{Ehmety01,
	Author = {Sidi O. Ehmety and Lawrence C. Paulson},
	Booktitle = {Theorem Proving in Higher Order Logics},
	Editor = {Richard J. Boulton and Paul B. Jackson},
	Pages = {151--158},
	Title = {{R}epresenting {C}omponent {S}tates in {H}igher-{O}rder {L}ogic},
	Year = {2001}}

@inproceedings{Devillers97,
	Author = {Marco Devillers and David Griffioen and Olaf M\"{u}ller},
	Booktitle = {10th International Conference on Theorem Proving in Higher Order Logics},
	Editor = {Elsa L. Gunter and Amy P. Felty},
	Month = {August},
	Pages = {89--104},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {{P}ossibly {I}nfinite {S}equences in {T}heorem {P}rovers: {A} Comparative Study},
	Volume = {1275},
	Year = {1997}}

@article{Lamport94,
	Author = {Leslie Lamport},
	Journal = {{ACM} {T}ransactions on {P}rogramming {L}anguages and {S}ystems},
	Month = may,
	Number = {3},
	Pages = {872--923},
	Title = {{T}he {T}emporal {L}ogic of {A}ctions},
	Volume = {16},
	Year = {1994}}

@inproceedings{Wildmoser04,
	Author = {Martin Wildmoser and Tobias Nipkow},
	Booktitle = {Theorem Proving in Higher Order Logics (TPHOLs 2004)},
	Editor = {K. Slind and A. Bunker and G. Gopalakrishnan},
	Pages = {305-320},
	Publisher = {Springer},
	Series = {LNCS},
	Title = {{C}ertifying {M}achine {C}ode {S}afety: {S}hallow versus {D}eep {E}mbedding},
	Volume = 3223,
	Year = 2004}

@inproceedings{Merz99,
	Address = {Toulouse, France},
	Author = {Stephan Merz},
	Booktitle = {FM'99: {W}orld {C}ongress on {F}ormal {M}ethods},
	Editor = {J.M. Wing and J. Woodcock and J. Davies},
	Month = sep,
	Pages = {1226--1244},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {{A} {M}ore {C}omplete {TLA}},
	Volume = 1709,
	Year = 1999}

@misc{Wenzel00b,
	Author = {Markus Wenzel},
	Month = May,
	Title = {{U}sing {A}xiomatic {T}ype {C}lasses in {I}sabelle},
	Year = {2000}}

@book{Lamport02,
	Address = {Reading, Massachusetts},
	Author = {Leslie Lamport},
	Publisher = {Addison-Wesley},
	Title = {Specifying Systems --- The TLA+ Language and Tools for Hardware and Software Engineers},
	Year = {2002}}

@unpublished{Merz98,
	Author = {Stephan Merz},
	Note = {http://www.pst.informatik.uni-muenchen.de/\~{}merz/isabelle/. Part of the Isabelle distribution.},
	Title = {{A}n {E}ncoding of {TLA} in {I}sabelle},
	Year = {1998}}

@InProceedings{chaudhuri:tlaps,
  author =       {Kaustuv Chaudhuri and Damien Doligez and Leslie Lamport and Stephan Merz},
  title =        {Verifying Safety Properties with the TLA\textsuperscript{+} Proof System},
  booktitle = {5th Intl. Joint Conf. Automated Reasoning (IJCAR 2010)},
  pages =     {142-148},
  year =      2010,
  editor =    {J{\"u}rgen Giesl and Reiner H{\"a}hnle},
  volume =    6173,
  series =    {Lecture Notes in Computer Science},
  address =   {Edinburgh, UK},
  publisher = {Springer},
}