1.1 --- a/doc-src/manual.bib Thu Oct 22 09:50:29 2009 +0200
1.2 +++ b/doc-src/manual.bib Thu Oct 22 14:45:20 2009 +0200
1.3 @@ -49,7 +49,7 @@
1.4
1.5 @Unpublished{abrial93,
1.6 author = {J. R. Abrial and G. Laffitte},
1.7 - title = {Towards the Mechanization of the Proofs of some Classical
1.8 + title = {Towards the Mechanization of the Proofs of Some Classical
1.9 Theorems of Set Theory},
1.10 note = {preprint},
1.11 year = 1993,
1.12 @@ -73,6 +73,17 @@
1.13 crossref = {types93},
1.14 pages = {213-237}}
1.15
1.16 +@inproceedings{andersson-1993,
1.17 + author = "Arne Andersson",
1.18 + title = "Balanced Search Trees Made Simple",
1.19 + editor = "F. K. H. A. Dehne and N. Santoro and S. Whitesides",
1.20 + booktitle = "WADS 1993",
1.21 + series = LNCS,
1.22 + volume = {709},
1.23 + pages = "61--70",
1.24 + year = 1993,
1.25 + publisher = Springer}
1.26 +
1.27 @book{andrews86,
1.28 author = "Peter Andrews",
1.29 title = "An Introduction to Mathematical Logic and Type Theory: to Truth
1.30 @@ -167,6 +178,15 @@
1.31 author = "Stefan Berghofer and Tobias Nipkow",
1.32 pages = "38--52"}
1.33
1.34 +@inproceedings{berghofer-nipkow-2004,
1.35 + author = {Stefan Berghofer and Tobias Nipkow},
1.36 + title = {Random Testing in {I}sabelle/{HOL}},
1.37 + pages = {230--239},
1.38 + editor = "J. Cuellar and Z. Liu",
1.39 + booktitle = {{SEFM} 2004},
1.40 + publisher = IEEE,
1.41 + year = 2004}
1.42 +
1.43 @InProceedings{Berghofer-Nipkow:2002,
1.44 author = {Stefan Berghofer and Tobias Nipkow},
1.45 title = {Executing Higher Order Logic},
1.46 @@ -200,6 +220,14 @@
1.47 title="Introduction to Functional Programming using Haskell",
1.48 publisher=PH,year=1998}
1.49
1.50 +@inproceedings{blanchette-nipkow-2009,
1.51 + title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder (Extended Abstract)",
1.52 + author = "Jasmin Christian Blanchette and Tobias Nipkow",
1.53 + booktitle = "{TAP} 2009: Short Papers",
1.54 + editor = "Catherine Dubois",
1.55 + publisher = "ETH Technical Report 630",
1.56 + year = 2009}
1.57 +
1.58 @Article{boyer86,
1.59 author = {Robert Boyer and Ewing Lusk and William McCune and Ross
1.60 Overbeek and Mark Stickel and Lawrence Wos},
1.61 @@ -241,7 +269,7 @@
1.62 }
1.63
1.64 @InProceedings{bulwahn-et-al:2008:imperative,
1.65 - author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews},
1.66 + author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews},
1.67 title = {Imperative Functional Programming with {Isabelle/HOL}},
1.68 crossref = {tphols2008},
1.69 }
1.70 @@ -597,6 +625,12 @@
1.71 year = 2003,
1.72 note = {\url{http://www.haskell.org/definition/}}}
1.73
1.74 +@book{jackson-2006,
1.75 + author = "Daniel Jackson",
1.76 + title = "Software Abstractions: Logic, Language, and Analysis",
1.77 + publisher = MIT,
1.78 + year = 2006}
1.79 +
1.80 %K
1.81
1.82 @InProceedings{kammueller-locales,
1.83 @@ -878,10 +912,11 @@
1.84
1.85 @Book{isa-tutorial,
1.86 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
1.87 - title = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
1.88 - publisher = {Springer},
1.89 + title = {Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic},
1.90 + publisher = Springer,
1.91 year = 2002,
1.92 - note = {LNCS Tutorial 2283}}
1.93 + series = LNCS,
1.94 + volume = 2283}
1.95
1.96 @Article{noel,
1.97 author = {Philippe No{\"e}l},
1.98 @@ -1021,7 +1056,7 @@
1.99 Essays in Honor of {Robin Milner}},
1.100 booktitle = {Proof, Language, and Interaction:
1.101 Essays in Honor of {Robin Milner}},
1.102 - publisher = {MIT Press},
1.103 + publisher = MIT,
1.104 year = 2000,
1.105 editor = {Gordon Plotkin and Colin Stirling and Mads Tofte}}
1.106
1.107 @@ -1236,6 +1271,12 @@
1.108 number = 4
1.109 }
1.110
1.111 +@misc{sledgehammer-2009,
1.112 + key = "Sledgehammer",
1.113 + title = "The {S}ledgehammer: Let Automatic Theorem Provers
1.114 +Write Your {I}s\-a\-belle Scripts",
1.115 + note = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/sledgehammer.html}"}
1.116 +
1.117 @inproceedings{slind-tfl,
1.118 author = {Konrad Slind},
1.119 title = {Function Definition in Higher Order Logic},
1.120 @@ -1295,6 +1336,27 @@
1.121 title={Haskell: The Craft of Functional Programming},
1.122 publisher={Addison-Wesley},year=1999}
1.123
1.124 +@misc{kodkod-2009,
1.125 + author = "Emina Torlak",
1.126 + title = {Kodkod: Constraint Solver for Relational Logic},
1.127 + note = "\url{http://alloy.mit.edu/kodkod/}"}
1.128 +
1.129 +@misc{kodkod-2009-options,
1.130 + author = "Emina Torlak",
1.131 + title = "Kodkod {API}: Class {Options}",
1.132 + note = "\url{http://alloy.mit.edu/kodkod/docs/kodkod/engine/config/Options.html}"}
1.133 +
1.134 +@inproceedings{torlak-jackson-2007,
1.135 + title = "Kodkod: A Relational Model Finder",
1.136 + author = "Emina Torlak and Daniel Jackson",
1.137 + editor = "Orna Grumberg and Michael Huth",
1.138 + booktitle = "TACAS 2007",
1.139 + series = LNCS,
1.140 + volume = {4424},
1.141 + pages = "632--647",
1.142 + year = 2007,
1.143 + publisher = Springer}
1.144 +
1.145 @Unpublished{Trybulec:1993:MizarFeatures,
1.146 author = {A. Trybulec},
1.147 title = {Some Features of the {Mizar} Language},
1.148 @@ -1320,6 +1382,13 @@
1.149 year = 1989
1.150 }
1.151
1.152 +@phdthesis{weber-2008,
1.153 + author = "Tjark Weber",
1.154 + title = "SAT-Based Finite Model Generation for Higher-Order Logic",
1.155 + school = {Dept.\ of Informatics, T.U. M\"unchen},
1.156 + type = "{Ph.D.}\ thesis",
1.157 + year = 2008}
1.158 +
1.159 @Misc{x-symbol,
1.160 author = {Christoph Wedler},
1.161 title = {Emacs package ``{X-Symbol}''},
1.162 @@ -1570,7 +1639,7 @@
1.163 Essays in Honor of {Larry Wos}},
1.164 booktitle = {Automated Reasoning and its Applications:
1.165 Essays in Honor of {Larry Wos}},
1.166 - publisher = {MIT Press},
1.167 + publisher = MIT,
1.168 year = 1997,
1.169 editor = {Robert Veroff}}
1.170
1.171 @@ -1669,3 +1738,8 @@
1.172 title = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
1.173 author = {Stefan Wehr et. al.}
1.174 }
1.175 +
1.176 +@misc{wikipedia-2009-aa-trees,
1.177 + key = "Wikipedia",
1.178 + title = "Wikipedia: {AA} Tree",
1.179 + note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}