@Misc{Bornat-lecture, author = {Richard Bornat}, title = {In defence of programming}, 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 = {Alexander 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 = {Tobias Nipkow and Lawrence C. Paulson and Markus 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 = {Norbert 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 = {Helmut 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 = {Christian Urban and Stefan 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 = {Philip 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 = {Makarius Wenzel}, title = {The {Isabelle/Isar} Implementation}, institution = {Technische Universit\"at M\"unchen}, note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}