@Misc{Bornat-lecture,

  author =	 {R.~Bornat},

  title =	 {In {D}efence of {P}rogramming},

  howpublished = {Available online via

                  \url{http://www.cs.mdx.ac.uk/staffpages/r_bornat/lectures/ revisedinauguraltext.pdf}},

  month =	 {April},

  year =	 2005,

  note =	 {Corrected and revised version of inaugural lecture,

                  delivered on 22nd January 2004 at the School of

                  Computing Science, Middlesex University}

}

@Book{isa-tutorial,

  author	= {T.~Nipkow and L.~C.~Paulson and M.~Wenzel},

  title		= {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},

  publisher	= {Springer},

  year		= 2002,

  note		= {LNCS Tutorial 2283}}

@book{paulson-ml2,

  author	= {Lawrence C. Paulson},

  title		= {{ML} for the Working Programmer},

  year		= 1996,

  edition	= {2nd},

  publisher	= {Cambridge University Press}}

@manual{isa-imp,

  author	= {M.~Wenzel},

  title		= {The {Isabelle/Isar} Implementation},

  institution	= {Technische Universit\"at M\"unchen},

  note          = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}

@book{GordonMilnerWadsworth79,

  author    = {M.~Gordon and R.~Milner and C.~P.~Wadsworth},

  title     = {{E}dinburgh {LCF}},

  publisher = {Springer},

  series    = {Lecture Notes in Computer Science},

  volume    = {78},

  year      = {1979}

}

@Article{Oppen80,

  author = 	 {D.~C.~Oppen},

  title = 	 {Pretty Printing},

  journal = 	 {ACM Transactions on Programming Languages and Systems},

  year = 	 {1980},

  pages = 	 {465--483}

}

@Article{ Dyckhoff92,

	title = "{Contraction-Free Sequent Calculi for Intuitionistic Logic}",

	author = "R. Dyckhoff",

	journal = "The Journal of Symbolic Logic",

	volume = "57",

	number = "3",

	pages = "795--807",

	year = "1992",

	publisher = "JSTOR"

}