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