@Comment public bib starts


@InProceedings{ridge05verifiedProver,
author="Tom Ridge and James Margetson",
title="A Mechanically Verified, Sound and Complete Theorem Prover for {FOL}",
  BOOKTITLE = {18th International Conference on Theorem Proving in Higher Order Logics: {TPHOLs} 2005},
  EDITOR = {Joe Hurd and Tom Melham},
  MONTH = AUG,
  YEAR = 2005,
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 3603,
noTeXtra={ <a href="doc/prover.pdf">prover.pdf</a> }
}


@InProceedings{conf/icnp/BiltcliffeDJRS06,
  OPTkey = ridge06icnp,
  title =	"Rigorous Protocol Design in Practice: An Optical
		 Packet-Switch {MAC} in {HOL}",
  author =	"Adam Biltcliffe and Michael Dales and Sam Jansen and
		 Tom Ridge and Peter Sewell",
  publisher =	"IEEE Computer Society",
  year = 	"2006",
  bibdate =	"2008-04-03",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/icnp/icnp2006.html#BiltcliffeDJRS06",
  booktitle =	"ICNP",
  OPTcrossref =	"conf/icnp/2006",
  ISBN = 	"1-4244-0593-9",
  pages =	"117--126",
  noTeXtra = { <a href="doc/ridge06icnp.pdf">ridge06icnp.pdf</a> }
}

@Comment   URL =  	"http://doi.ieeecomputersociety.org/10.1109/ICNP.2006.320205",

@Misc{ridge06poplmark,
  author = 	 {Tom Ridge},
  title = 	 {A solution to the {POPLmark} challenge 1a using de {Bruijn} notation.},
  howpublished = {Available online at \url{http://www.cl.cam.ac.uk/~tjr22}},
  year = 	 {2006},
  note="Isabelle/HOL proof scripts."
}

@InProceedings{conf/tphol/Ridge07,
  OPTkey = ridge07operational,
  title =	"Operational Reasoning for Concurrent {Caml} Programs and
		 Weak Memory Models",
  author =	"Tom Ridge",
  bibdate =	"2007-08-29",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/tphol/tphol2007.html#Ridge07",
  booktitle =	"Theorem Proving in Higher Order Logics, 20th
		 International Conference, {TPHOL}s 2007,
		 Kaiserslautern, Germany, September 10-13, 2007,
		 Proceedings",
  publisher =	"Springer",
  year = 	"2007",
  volume =	"4732",
  editor =	"Klaus Schneider and Jens Brandt",
  ISBN = 	"978-3-540-74590-7",
  pages =	"278--293",
  series =	"Lecture Notes in Computer Science",
  noTeXtra = { <a href="doc/ridge07tphols.pdf">ridge07tphols.pdf</a> }
}
@Comment  URL =  	"http://dx.doi.org/10.1007/978-3-540-74591-4_21",

@InProceedings{ridge07wmm,
  author =       {Tom Ridge},
  title =        {To arrive where we started: experience of mechanizing binding},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Proceedings of the {Workshop on Mechanizing Metatheory}},
  year =         {2007},
  month =        oct,
  noTeXtra = { <a href="doc/ridge07wmm.pdf">ridge07wmm.pdf</a> }
}


@InProceedings{conf/fm/RidgeNS08,
  title =	"A Rigorous Approach to Networking: {TCP}, from
		 Implementation to Protocol to Service",
  author =	"Tom Ridge and Michael Norrish and Peter Sewell",
  bibdate =	"2008-06-09",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/fm/fm2008.html#RidgeNS08",
  booktitle =	"FM",
  booktitle =	"{FM} 2008: Formal Methods, 15th International
		 Symposium on Formal Methods, Turku, Finland, May 26-30,
		 2008, Proceedings",
  publisher =	"Springer",
  year = 	"2008",
  volume =	"5014",
  editor =	"Jorge Cu{\'e}llar and T. S. E. Maibaum and Kaisa
		 Sere",
  ISBN = 	"978-3-540-68235-6",
  pages =	"294--309",
  series =	"Lecture Notes in Computer Science",
  noTeXtra = {<a href="doc/ridge08stream-spec.pdf">ridge08stream-spec.pdf</a>}
}

@Comment  URL =  	"http://dx.doi.org/10.1007/978-3-540-68237-0_21",


@InProceedings{conf/icfp/SewellNOPRSS07,
  title =	"Ott: effective tool support for the working
		 semanticist",
  author =	"Peter Sewell and Francesco Zappa Nardelli and Scott
		 Owens and Gilles Peskine and Tom Ridge and Susmit
		 Sarkar and Rok Strnisa",
  bibdate =	"2007-11-06",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/icfp/icfp2007.html#SewellNOPRSS07",
  booktitle =	"ICFP",
  booktitle =	"Proceedings of the 12th {ACM} {SIGPLAN} International
		 Conference on Functional Programming, {ICFP} 2007,
		 Freiburg, Germany, October 1-3, 2007",
  publisher =	"ACM",
  year = 	"2007",
  editor =	"Ralf Hinze and Norman Ramsey",
  ISBN = 	"978-1-59593-815-2",
  pages =	"1--12",
  noTeXtra = {<a href="doc/ott.pdf">ott.pdf</a>}
}

@Comment  URL =  	"http://doi.acm.org/10.1145/1291151.1291155",


@InProceedings{conf/popl/Ridge09,
  title =	"Verifying distributed systems: the operational
		 approach",
  author =	"Tom Ridge",
  bibdate =	"2009-01-24",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/popl/popl2009.html#Ridge09",
  booktitle =	"POPL",
  booktitle =	"Proceedings of the 36th {ACM} {SIGPLAN}-{SIGACT}
		 Symposium on Principles of Programming Languages,
		 {POPL} 2009, Savannah, {GA}, {USA}, January 21-23,
		 2009",
  publisher =	"ACM",
  year = 	"2009",
  editor =	"Zhong Shao and Benjamin C. Pierce",
  ISBN = 	"978-1-60558-379-2",
  pages =	"429--440",
  noTeX = "Keywords: verified, mechanized, formal, message, queue, OCaml",
  noTeXtra = {<a href="doc/ridge09popl.pdf">ridge09popl.pdf</a>}

}

@Comment  URL =  	"http://doi.acm.org/10.1145/1480881.1480934",

@InProceedings{conf/popl/SarkarSNORBMA09,
  title =	"The semantics of x86-{CC} multiprocessor machine
		 code",
  author =	"Susmit Sarkar and Peter Sewell and Francesco Zappa
		 Nardelli and Scott Owens and Tom Ridge and Thomas
		 Braibant and Magnus O. Myreen and Jade Alglave",
  bibdate =	"2009-01-24",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/popl/popl2009.html#SarkarSNORBMA09",
  booktitle =	"POPL",
  booktitle =	"Proceedings of the 36th {ACM} {SIGPLAN}-{SIGACT}
		 Symposium on Principles of Programming Languages,
		 {POPL} 2009, Savannah, {GA}, {USA}, January 21-23,
		 2009",
  publisher =	"ACM",
  year = 	"2009",
  editor =	"Zhong Shao and Benjamin C. Pierce",
  ISBN = 	"978-1-60558-379-2",
  pages =	"379--391",
  noTeXtra = {<a href="doc/popl09.pdf">popl09.pdf</a>}
}

@Comment   URL =  	"http://doi.acm.org/10.1145/1480881.1480929",

@article{ott-jfp,
 author =       {Peter Sewell and Zappa Nardelli, Francesco  and Scott Owens and Gilles Peskine and Thomas Ridge and Susmit Sarkar and Rok Strni\v sa},
 title =        {{Ott}: Effective Tool Support for the Working Semanticist},
 journal =      {Journal of Functional Programming},
 year =         {2010},
 volume =       {20},
 number =       {1},
 pages =        {70--122},
 month =        jan,
 note =         {Invited submission from ICFP 2007},
 noTeXtra = {<a href="doc/ridge10ott-jfp.pdf">ridge10ott-jfp.pdf</a>}
}

@inproceedings{DBLP:conf/vstte/Ridge10,
  author    = {Tom Ridge},
  title     = {A Rely-Guarantee Proof System for x86-{TSO}},
  booktitle = {VSTTE},
  year      = {2010},
  pages     = {55-70},
  ee        = {http://dx.doi.org/10.1007/978-3-642-15057-9_4},
  crossref  = {DBLP:conf/vstte/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  noTeXtra = {<a href="doc/ridge10vstte.pdf">ridge10vstte.pdf</a>}
}

@proceedings{DBLP:conf/vstte/2010,
  editor    = {Gary T. Leavens and
               Peter O'Hearn and
               Sriram K. Rajamani},
  title     = {Verified Software: Theories, Tools, Experiments, Third International
               Conference, VSTTE 2010, Edinburgh, UK, August 16-19, 2010.
               Proceedings},
  booktitle = {VSTTE},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6217},
  year      = {2010},
  isbn      = {978-3-642-15056-2},
  ee        = {http://dx.doi.org/10.1007/978-3-642-15057-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@InProceedings{ridge10parsing,
  title =	"Simple, functional, sound and complete parsing for all context-free grammars (unpublished draft)",
  author =	"Tom Ridge",
  note="Unpublished draft",
  noTeXtra = {<a href="doc/ridge10parsing.pdf">ridge10parsing.pdf</a>}
}


@inproceedings{ridge11parsing-cpp,
  author    = {Tom Ridge},
  title     = {Simple, Functional, Sound and Complete Parsing for All Context-Free
               Grammars},
  booktitle = {CPP},
  year      = {2011},
  pages     = {103-118},
  ee        = {http://dx.doi.org/10.1007/978-3-642-25379-9_10},
  crossref  = {DBLP:conf/cpp/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  noTeX = "Keywords: verified, mechanized, formal, parsing, sound, complete, functional, combinator",
  noTeXtra = {[<a href="http://tom-ridge.blogspot.com/2011/06/simple-functional-sound-and-complete_22.html">Read more</a>] [<a href="parsing/index.html">additional material</a>]},
  ignorenoTeXtra = {<a href="doc/ridge11parsing-cpp.pdf">ridge11parsing-cpp.pdf</a>. See also <a href="parsing/index.html">here</a>.}
}
@proceedings{DBLP:conf/cpp/2011,
  editor    = {Jean-Pierre Jouannaud and
               Zhong Shao},
  title     = {Certified Programs and Proofs - First International Conference,
               CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
  booktitle = {CPP},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7086},
  year      = {2011},
  isbn      = {978-3-642-25378-2},
  ee        = {http://dx.doi.org/10.1007/978-3-642-25379-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{vscomp2010,
  author    = {Vladimir Klebanov and
               Peter M{\"u}ller and
               Natarajan Shankar and
               Gary T. Leavens and
               Valentin W{\"u}stholz and
               Eyad Alkassar and
               Rob Arthan and
               Derek Bronish and
               Rod Chapman and
               Ernie Cohen and
               Mark Hillebrand and
               Bart Jacobs and
               K. Rustan M. Leino and
               Rosemary Monahan and
               Frank Piessens and
               Nadia Polikarpova and
               Tom Ridge and
               Jan Smans and
               Stephan Tobies and
               Thomas Tuerk and
               Mattias Ulbrich and
               Benjamin Wei{\ss}},
  title     = {The 1st {V}erified {S}oftware {C}ompetition: Experience Report},
  booktitle = {Proceedings, 17th International Symposium on Formal Methods (FM 2011)},
  editor    = {Michael Butler and Wolfram Schulte},
  year      = {2011},
  note      = {To appear. Materials available at \url{www.vscomp.org}.},
  noTeXtra = {[<a href="http://tom-ridge.blogspot.com/2011/06/1st-verified-software-competition.html">paper and additional material</a>]}

}


@Comment   booktitle =	"POPL",
@Comment   booktitle =	"Proceedings of the 38th {ACM} {SIGPLAN}-{SIGACT}
@Comment 		 Symposium on Principles of Programming Languages,
@Comment 		 {POPL} 2009, Austin, {TX}, {USA}, January 26-28,
@Comment 		 2009",
@Comment   publisher =	"ACM",
@Comment   year = 	"2011",



@Comment public bib ends