--- a/CookBook/document/root.bib Fri Oct 10 17:09:17 2008 +0200
+++ b/CookBook/document/root.bib Fri Oct 10 17:11:46 2008 +0200
@@ -1,10 +1,44 @@
+@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}
+}
-@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}}}
+@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},
@@ -18,4 +52,77 @@
title = {{ML} for the Working Programmer},
year = 1996,
edition = {2nd},
- publisher = {Cambridge University Press}}
\ No newline at end of file
+ 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}}}