diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/document/root.bib --- a/CookBook/document/root.bib Wed Mar 18 23:52:51 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,138 +0,0 @@ -@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} -} \ No newline at end of file