--- a/doc-src/manual.bib Thu Oct 22 09:50:29 2009 +0200
+++ b/doc-src/manual.bib Thu Oct 22 14:45:20 2009 +0200
@@ -49,7 +49,7 @@
@Unpublished{abrial93,
author = {J. R. Abrial and G. Laffitte},
- title = {Towards the Mechanization of the Proofs of some Classical
+ title = {Towards the Mechanization of the Proofs of Some Classical
Theorems of Set Theory},
note = {preprint},
year = 1993,
@@ -73,6 +73,17 @@
crossref = {types93},
pages = {213-237}}
+@inproceedings{andersson-1993,
+ author = "Arne Andersson",
+ title = "Balanced Search Trees Made Simple",
+ editor = "F. K. H. A. Dehne and N. Santoro and S. Whitesides",
+ booktitle = "WADS 1993",
+ series = LNCS,
+ volume = {709},
+ pages = "61--70",
+ year = 1993,
+ publisher = Springer}
+
@book{andrews86,
author = "Peter Andrews",
title = "An Introduction to Mathematical Logic and Type Theory: to Truth
@@ -167,6 +178,15 @@
author = "Stefan Berghofer and Tobias Nipkow",
pages = "38--52"}
+@inproceedings{berghofer-nipkow-2004,
+ author = {Stefan Berghofer and Tobias Nipkow},
+ title = {Random Testing in {I}sabelle/{HOL}},
+ pages = {230--239},
+ editor = "J. Cuellar and Z. Liu",
+ booktitle = {{SEFM} 2004},
+ publisher = IEEE,
+ year = 2004}
+
@InProceedings{Berghofer-Nipkow:2002,
author = {Stefan Berghofer and Tobias Nipkow},
title = {Executing Higher Order Logic},
@@ -200,6 +220,14 @@
title="Introduction to Functional Programming using Haskell",
publisher=PH,year=1998}
+@inproceedings{blanchette-nipkow-2009,
+ title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder (Extended Abstract)",
+ author = "Jasmin Christian Blanchette and Tobias Nipkow",
+ booktitle = "{TAP} 2009: Short Papers",
+ editor = "Catherine Dubois",
+ publisher = "ETH Technical Report 630",
+ year = 2009}
+
@Article{boyer86,
author = {Robert Boyer and Ewing Lusk and William McCune and Ross
Overbeek and Mark Stickel and Lawrence Wos},
@@ -241,7 +269,7 @@
}
@InProceedings{bulwahn-et-al:2008:imperative,
- author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews},
+ author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews},
title = {Imperative Functional Programming with {Isabelle/HOL}},
crossref = {tphols2008},
}
@@ -597,6 +625,12 @@
year = 2003,
note = {\url{http://www.haskell.org/definition/}}}
+@book{jackson-2006,
+ author = "Daniel Jackson",
+ title = "Software Abstractions: Logic, Language, and Analysis",
+ publisher = MIT,
+ year = 2006}
+
%K
@InProceedings{kammueller-locales,
@@ -878,10 +912,11 @@
@Book{isa-tutorial,
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
- title = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
- publisher = {Springer},
+ title = {Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic},
+ publisher = Springer,
year = 2002,
- note = {LNCS Tutorial 2283}}
+ series = LNCS,
+ volume = 2283}
@Article{noel,
author = {Philippe No{\"e}l},
@@ -1021,7 +1056,7 @@
Essays in Honor of {Robin Milner}},
booktitle = {Proof, Language, and Interaction:
Essays in Honor of {Robin Milner}},
- publisher = {MIT Press},
+ publisher = MIT,
year = 2000,
editor = {Gordon Plotkin and Colin Stirling and Mads Tofte}}
@@ -1236,6 +1271,12 @@
number = 4
}
+@misc{sledgehammer-2009,
+ key = "Sledgehammer",
+ title = "The {S}ledgehammer: Let Automatic Theorem Provers
+Write Your {I}s\-a\-belle Scripts",
+ note = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/sledgehammer.html}"}
+
@inproceedings{slind-tfl,
author = {Konrad Slind},
title = {Function Definition in Higher Order Logic},
@@ -1295,6 +1336,27 @@
title={Haskell: The Craft of Functional Programming},
publisher={Addison-Wesley},year=1999}
+@misc{kodkod-2009,
+ author = "Emina Torlak",
+ title = {Kodkod: Constraint Solver for Relational Logic},
+ note = "\url{http://alloy.mit.edu/kodkod/}"}
+
+@misc{kodkod-2009-options,
+ author = "Emina Torlak",
+ title = "Kodkod {API}: Class {Options}",
+ note = "\url{http://alloy.mit.edu/kodkod/docs/kodkod/engine/config/Options.html}"}
+
+@inproceedings{torlak-jackson-2007,
+ title = "Kodkod: A Relational Model Finder",
+ author = "Emina Torlak and Daniel Jackson",
+ editor = "Orna Grumberg and Michael Huth",
+ booktitle = "TACAS 2007",
+ series = LNCS,
+ volume = {4424},
+ pages = "632--647",
+ year = 2007,
+ publisher = Springer}
+
@Unpublished{Trybulec:1993:MizarFeatures,
author = {A. Trybulec},
title = {Some Features of the {Mizar} Language},
@@ -1320,6 +1382,13 @@
year = 1989
}
+@phdthesis{weber-2008,
+ author = "Tjark Weber",
+ title = "SAT-Based Finite Model Generation for Higher-Order Logic",
+ school = {Dept.\ of Informatics, T.U. M\"unchen},
+ type = "{Ph.D.}\ thesis",
+ year = 2008}
+
@Misc{x-symbol,
author = {Christoph Wedler},
title = {Emacs package ``{X-Symbol}''},
@@ -1570,7 +1639,7 @@
Essays in Honor of {Larry Wos}},
booktitle = {Automated Reasoning and its Applications:
Essays in Honor of {Larry Wos}},
- publisher = {MIT Press},
+ publisher = MIT,
year = 1997,
editor = {Robert Veroff}}
@@ -1669,3 +1738,8 @@
title = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
author = {Stefan Wehr et. al.}
}
+
+@misc{wikipedia-2009-aa-trees,
+ key = "Wikipedia",
+ title = "Wikipedia: {AA} Tree",
+ note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}