@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}}@Misc{wenzel-technology, author = {M.~Wenzel}, title = {Further Scaling of Isabelle Technology}, howpublished = {http://sketis.net}, month = {April}, year = {2018}, note = {},}@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"}