@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"
}