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

}

@inproceedings{Krauss-IJCAR06,

  author =	 {A.~Krauss},

  title =	 {{P}artial {R}ecursive {F}unctions in {H}igher-{O}rder {L}ogic},

  editor =	 {Ulrich Furbach and Natarajan Shankar},

  booktitle =	 {Automated Reasoning, Third International Joint

                  Conference, IJCAR 2006, Seattle, WA, USA, August

                  17-20, 2006, Proceedings},

  publisher =	 {Springer-Verlag},

  series =	 {Lecture Notes in Computer Science},

  volume =	 {4130},

  year =	 {2006},

  pages =	 {589-603}

}

@INPROCEEDINGS{Melham:1992:PIR,

  AUTHOR =	 {T.~F.~Melham},

  TITLE =	 {{A} {P}ackage for {I}nductive {R}elation {D}efinitions in

                  {HOL}},

  BOOKTITLE =	 {Proceedings of the 1991 International Workshop on

                  the {HOL} Theorem Proving System and its

                  Applications, {D}avis, {C}alifornia, {A}ugust

                  28--30, 1991},

  EDITOR =	 {Myla Archer and Jeffrey J. Joyce and Karl N. Levitt

                  and Phillip J. Windley},

  PUBLISHER =	 {IEEE Computer Society Press},

  YEAR =	 {1992},

  PAGES =	 {350--357},

  ISBN =	 {0-8186-2460-4},

}

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

@InCollection{Paulson-ind-defs,

  author =	 {L.~C.~Paulson},

  title =	 {A fixedpoint approach to (co)inductive and

                  (co)datatype definitions},

  booktitle =	 {Proof, Language, and Interaction: Essays in Honour

                  of Robin Milner},

  pages =	 {187--211},

  publisher =	 {MIT Press},

  year =	 2000,

  editor =	 {G. Plotkin and C. Stirling and M. Tofte}

}

@inproceedings{Schirmer-LPAR04,

  author =	 {N.~Schirmer},

  title =	 {{A} {V}erification {E}nvironment for {S}equential {I}mperative

                  Programs in {I}sabelle/{HOL}},

  booktitle =	 "Logic for Programming, Artificial Intelligence, and

                  Reasoning",

  editor =	 "F. Baader and A. Voronkov",

  year =	 2005,

  publisher =	 "Springer-Verlag",

  series =	 "Lecture Notes in Artificial Intelligence",

  volume =	 3452,

  pages =	 {398--414}

}

@TechReport{Schwichtenberg-MLCF,

  author =	 {H.~Schwichtenberg},

  title =	 {{M}inimal {L}ogic {f}or {C}omputable {F}unctionals},

  institution =	 {Mathematisches Institut,

                  Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen},

  year =	 2005,

  month =	 {December},

  note =	 {Available online at

                  \url{http://www.mathematik.uni-muenchen.de/~minlog/minlog/mlcf.pdf}}

}

@inproceedings{Urban-Berghofer06,

  author =	 {C.~Urban and S.~Berghofer},

  title =	 {{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes

                  {I}mplemented in {I}sabelle/{HOL}},

  editor =	 {Ulrich Furbach and Natarajan Shankar},

  booktitle =	 {Automated Reasoning, Third International Joint

                  Conference, IJCAR 2006, Seattle, WA, USA, August

                  17-20, 2006, Proceedings},

  publisher =	 {Springer-Verlag},

  series =	 {Lecture Notes in Computer Science},

  volume =	 {4130},

  year =	 {2006},

  pages =	 {498-512}

}

@inproceedings{Wadler-AFP95,

  author =	 {P.~Wadler},

  title =	 {Monads for Functional Programming},

  pages =	 {24-52},

  editor =	 {Johan Jeuring and Erik Meijer},

  booktitle =	 {Advanced Functional Programming, First International

                  Spring School on Advanced Functional Programming

                  Techniques, B{\aa}stad, Sweden, May 24-30, 1995,

                  Tutorial Text},

  publisher =	 {Springer-Verlag},

  series =	 {Lecture Notes in Computer Science},

  volume =	 {925},

  year =	 {1995}

}

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

}