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