author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 56363  89e0264adf79 
child 57241  7fca4159117f 
permissions  rwrr 
6592  1 
% BibTeX database for the Isabelle documentation 
2 

3 
%publishers 

4 
@string{AP="Academic Press"} 

5 
@string{CUP="Cambridge University Press"} 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
33926
diff
changeset

6 
@string{IEEE="IEEE Computer Society Press"} 
11199  7 
@string{LNCS="Lecture Notes in Computer Science"} 
6592  8 
@string{MIT="MIT Press"} 
9 
@string{NH="NorthHolland"} 

10 
@string{Prentice="PrenticeHall"} 

6607  11 
@string{PH="PrenticeHall"} 
6592  12 
@string{Springer="SpringerVerlag"} 
13 

14 
%institutions 

11199  15 
@string{CUCL="Computer Laboratory, University of Cambridge"} 
16 
@string{Edinburgh="Department of Computer Science, University of Edinburgh"} 

21074  17 
@string{TUM="Department of Informatics, Technical University of Munich"} 
6592  18 

19 
%journals 

8284  20 
@string{AI="Artificial Intelligence"} 
11199  21 
@string{FAC="Formal Aspects of Computing"} 
22 
@string{JAR="Journal of Automated Reasoning"} 

23 
@string{JCS="Journal of Computer Security"} 

24 
@string{JFP="Journal of Functional Programming"} 

25 
@string{JLC="Journal of Logic and Computation"} 

26 
@string{JLP="Journal of Logic Programming"} 

27 
@string{JSC="Journal of Symbolic Computation"} 

28 
@string{JSL="Journal of Symbolic Logic"} 

11246  29 
@string{PROYAL="Proceedings of the Royal Society of London"} 
6592  30 
@string{SIGPLAN="{SIGPLAN} Notices"} 
11246  31 
@string{TISSEC="ACM Transactions on Information and System Security"} 
6592  32 

33 
%conferences 

34 
@string{CADE="International Conference on Automated Deduction"} 

35 
@string{POPL="Symposium on Principles of Programming Languages"} 

36 
@string{TYPES="Types for Proofs and Programs"} 

37 

38 

39 
%A 

40 

41 
@incollection{abramsky90, 

42 
author = {Samson Abramsky}, 

43 
title = {The Lazy Lambda Calculus}, 

44 
pages = {65116}, 

45 
editor = {David A. Turner}, 

46 
booktitle = {Research Topics in Functional Programming}, 

47 
publisher = {AddisonWesley}, 

48 
year = 1990} 

49 

50 
@Unpublished{abrial93, 

51 
author = {J. R. Abrial and G. Laffitte}, 

33191  52 
title = {Towards the Mechanization of the Proofs of Some Classical 
6592  53 
Theorems of Set Theory}, 
54 
note = {preprint}, 

55 
year = 1993, 

56 
month = Feb} 

57 

58 
@incollection{aczel77, 

59 
author = {Peter Aczel}, 

60 
title = {An Introduction to Inductive Definitions}, 

61 
pages = {739782}, 

62 
crossref = {barwisehandbk}} 

63 

64 
@Book{aczel88, 

65 
author = {Peter Aczel}, 

66 
title = {NonWellFounded Sets}, 

67 
publisher = {CSLI}, 

68 
year = 1988} 

69 

39600  70 
@inproceedings{AehligHaftmannNipkow:2008:nbe, 
71 
author = {Klaus Aehlig and Florian Haftmann and Tobias Nipkow}, 

72 
title = {A Compiled Implementation of Normalization by Evaluation}, 

73 
booktitle = {TPHOLs '08: Proceedings of the 21th International Conference on Theorem Proving in Higher Order Logics}, 

74 
year = {2008}, 

75 
isbn = {9783540710653}, 

76 
pages = {352367}, 

77 
publisher = Springer, 

78 
series = LNCS, 

79 
volume = {5170}, 

80 
editor = {Otmane A\"{\i}t Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar} 

81 
} 

82 

6592  83 
@InProceedings{alf, 
84 
author = {Lena Magnusson and Bengt {Nordstr\"{o}m}}, 

85 
title = {The {ALF} Proof Editor and Its Proof Engine}, 

86 
crossref = {types93}, 

87 
pages = {213237}} 

88 

33191  89 
@inproceedings{andersson1993, 
90 
author = "Arne Andersson", 

91 
title = "Balanced Search Trees Made Simple", 

92 
editor = "F. K. H. A. Dehne and N. Santoro and S. Whitesides", 

93 
booktitle = "WADS 1993", 

94 
series = LNCS, 

95 
volume = {709}, 

96 
pages = "6170", 

97 
year = 1993, 

98 
publisher = Springer} 

99 

6592  100 
@book{andrews86, 
101 
author = "Peter Andrews", 

102 
title = "An Introduction to Mathematical Logic and Type Theory: to Truth 

103 
through Proof", 

104 
publisher = AP, 

105 
series = "Computer Science and Applied Mathematics", 

106 
year = 1986} 

107 

9599  108 
@InProceedings{Aspinall:2000:eProof, 
109 
author = {David Aspinall}, 

110 
title = {Protocols for Interactive {eProof}}, 

111 
booktitle = {Theorem Proving in Higher Order Logics (TPHOLs)}, 

112 
year = 2000, 

113 
note = {Unpublished workinprogress paper, 

14296
bcba1d67f854
updated references to the nowpornographic proofgeneral.org
paulson
parents:
14210
diff
changeset

114 
\url{http://homepages.inf.ed.ac.uk/da/papers/drafts/eproof.ps.gz}} 
9599  115 
} 
14296
bcba1d67f854
updated references to the nowpornographic proofgeneral.org
paulson
parents:
14210
diff
changeset

116 

8505  117 
@InProceedings{Aspinall:TACAS:2000, 
118 
author = {David Aspinall}, 

10160  119 
title = {{P}roof {G}eneral: A Generic Tool for Proof Development}, 
11205  120 
booktitle = {Tools and Algorithms for the Construction and Analysis of 
121 
Systems (TACAS)}, 

122 
year = 2000, 

123 
publisher = Springer, 

124 
series = LNCS, 

125 
volume = 1785, 

126 
pages = "3842" 

8505  127 
} 
128 

7209  129 
@Misc{isamode, 
130 
author = {David Aspinall}, 

8062  131 
title = {Isamode  {U}sing {I}sabelle with {E}macs}, 
14296
bcba1d67f854
updated references to the nowpornographic proofgeneral.org
paulson
parents:
14210
diff
changeset

132 
note = {\url{http://homepages.inf.ed.ac.uk/da/Isamode/}} 
7209  133 
} 
134 

135 
@Misc{proofgeneral, 

11197  136 
author = {David Aspinall}, 
137 
title = {{P}roof {G}eneral}, 

14296
bcba1d67f854
updated references to the nowpornographic proofgeneral.org
paulson
parents:
14210
diff
changeset

138 
note = {\url{http://proofgeneral.inf.ed.ac.uk/}} 
7209  139 
} 
140 

6592  141 
%B 
142 

44093  143 
@inproceedings{backesbrown2010, 
42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

144 
title = "Analytic Tableaux for HigherOrder Logic with Choice", 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

145 
author = "Julian Backes and Chad E. Brown", 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

146 
booktitle={Automated Reasoning: IJCAR 2010}, 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

147 
editor={J. Giesl and R. H\"ahnle}, 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

148 
publisher = Springer, 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

149 
series = LNCS, 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

150 
volume = 6173, 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

151 
pages = "7690", 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

152 
year = 2010} 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

153 

10186  154 
@book{BaaderNipkow,author={Franz Baader and Tobias Nipkow}, 
155 
title="Term Rewriting and All That",publisher=CUP,year=1998} 

156 

37429  157 
@manual{isabellelocale, 
158 
author = {Clemens Ballarin}, 

159 
title = {Tutorial to Locales and Locale Interpretation}, 

160 
institution = TUM, 

161 
note = {\url{http://isabelle.in.tum.de/doc/locales.pdf}} 

162 
} 

163 

55117  164 
@article{Ballarin2014, 
53370
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53125
diff
changeset

165 
author = {Ballarin, Clemens}, 
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53125
diff
changeset

166 
journal = JAR, 
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53125
diff
changeset

167 
publisher = Springer, 
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53125
diff
changeset

168 
title = {Locales: A Module System for Mathematical Theories}, 
55117  169 
volume = 52, 
170 
number = 2, 

171 
pages = {123153}, 

53370
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53125
diff
changeset

172 
url = {http://dx.doi.org/10.1007/s1081701392847}, 
55117  173 
year = {2014}} 
53370
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53125
diff
changeset

174 

20482  175 
@InCollection{BarendregtGeuvers:2001, 
176 
author = {H. Barendregt and H. Geuvers}, 

177 
title = {Proof Assistants using Dependent Type Systems}, 

178 
booktitle = {Handbook of Automated Reasoning}, 

179 
publisher = {Elsevier}, 

180 
year = 2001, 

181 
editor = {A. Robinson and A. Voronkov} 

182 
} 

183 

40942  184 
@inproceedings{cvc3, 
185 
author = {Clark Barrett and Cesare Tinelli}, 

186 
title = {{CVC3}}, 

187 
booktitle = {CAV}, 

188 
editor = {Werner Damm and Holger Hermanns}, 

189 
volume = {4590}, 

190 
series = LNCS, 

191 
pages = {298302}, 

192 
publisher = {Springer}, 

193 
year = {2007} 

194 
} 

195 

6592  196 
@incollection{basin91, 
197 
author = {David Basin and Matt Kaufmann}, 

198 
title = {The {BoyerMoore} Prover and {Nuprl}: An Experimental 

54583  199 
Comparison}, 
6592  200 
crossref = {huetplotkin91}, 
201 
pages = {89119}} 

202 

12466  203 
@Unpublished{HOLLibrary, 
204 
author = {Gertrud Bauer and Tobias Nipkow and Oheimb, David von and 

205 
Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and 

206 
Markus Wenzel}, 

207 
title = {The Supplemental {Isabelle/HOL} Library}, 

12660  208 
note = {Part of the Isabelle distribution, 
12466  209 
\url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, 
12660  210 
year = 2002 
12466  211 
} 
212 

9567  213 
@InProceedings{BauerWenzel:2000:HB, 
214 
author = {Gertrud Bauer and Markus Wenzel}, 

215 
title = {ComputerAssisted Mathematics at Work  The {H}ahn{B}anach Theorem in 

216 
{I}sabelle/{I}sar}, 

217 
booktitle = {Types for Proofs and Programs: TYPES'99}, 

9599  218 
editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m 
219 
and Jan Smith}, 

9567  220 
series = {LNCS}, 
9599  221 
year = 2000 
9567  222 
} 
6624  223 

12878  224 
@InProceedings{BauerWenzel:2001, 
225 
author = {Gertrud Bauer and Markus Wenzel}, 

226 
title = {Calculational reasoning revisited  an {Isabelle/Isar} experience}, 

227 
crossref = {tphols2001}} 

228 

42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

229 
@inproceedings{leo2, 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

230 
author = "Christoph Benzm{\"u}ller and Lawrence C. Paulson and Frank Theiss and Arnaud Fietzke", 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

231 
title = "{LEOII}A Cooperative Automatic Theorem Prover for HigherOrder Logic", 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

232 
editor = "Alessandro Armando and Peter Baumgartner and Gilles Dowek", 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

233 
booktitle = "Automated Reasoning: IJCAR 2008", 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

234 
publisher = Springer, 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

235 
series = LNCS, 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

236 
volume = 5195, 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

237 
pages = "162170", 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

238 
year = 2008} 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

239 

33926
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

240 
@inProceedings{BerghoferBulwahnHaftmann:2009:TPHOL, 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

241 
author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian}, 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

242 
booktitle = {Theorem Proving in Higher Order Logics}, 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

243 
pages = {131146}, 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

244 
title = {Turning Inductive into Equational Specifications}, 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

245 
year = {2009} 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

246 
} 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

247 

11619  248 
@INPROCEEDINGS{BerghoferNipkow:2000:TPHOL, 
249 
crossref = "tphols2000", 

250 
title = "Proof terms for simply typed higher order logic", 

251 
author = "Stefan Berghofer and Tobias Nipkow", 

252 
pages = "3852"} 

253 

33191  254 
@inproceedings{berghofernipkow2004, 
255 
author = {Stefan Berghofer and Tobias Nipkow}, 

256 
title = {Random Testing in {I}sabelle/{HOL}}, 

257 
pages = {230239}, 

258 
editor = "J. Cuellar and Z. Liu", 

259 
booktitle = {{SEFM} 2004}, 

260 
publisher = IEEE, 

261 
year = 2004} 

262 

12612  263 
@InProceedings{BerghoferNipkow:2002, 
264 
author = {Stefan Berghofer and Tobias Nipkow}, 

265 
title = {Executing Higher Order Logic}, 

266 
booktitle = {Types for Proofs and Programs: TYPES'2000}, 

267 
editor = {P. Callaghan and Z. Luo and J. McKinna and R. Pollack}, 

268 
series = LNCS, 

269 
publisher = Springer, 

13009  270 
volume = 2277, 
12612  271 
year = 2002} 
272 

6624  273 
@InProceedings{BerghoferWenzel:1999:TPHOL, 
274 
author = {Stefan Berghofer and Markus Wenzel}, 

7041  275 
title = {Inductive datatypes in {HOL}  lessons learned in 
276 
{F}ormal{L}ogic {E}ngineering}, 

277 
crossref = {tphols99}} 

6624  278 

30170  279 

280 
@InProceedings{BezemCoquand:2005, 

281 
author = {M.A. Bezem and T. Coquand}, 

282 
title = {Automating {Coherent Logic}}, 

283 
booktitle = {LPAR12}, 

284 
editor = {G. Sutcliffe and A. Voronkov}, 

285 
volume = 3835, 

286 
series = LNCS, 

287 
publisher = Springer} 

288 

6607  289 
@book{BirdWadler,author="Richard Bird and Philip Wadler", 
290 
title="Introduction to Functional Programming",publisher=PH,year=1988} 

291 

11209  292 
@book{BirdHaskell,author="Richard Bird", 
293 
title="Introduction to Functional Programming using Haskell", 

294 
publisher=PH,year=1998} 

295 

42215
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

296 
@manual{isabellenitpick, 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

297 
author = {Jasmin Christian Blanchette}, 
53647  298 
title = {Picking Nits: A User's Guide to {N}itpick for {I}sabelle\slash {HOL}}, 
42215
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

299 
institution = TUM, 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

300 
note = {\url{http://isabelle.in.tum.de/doc/nitpick.pdf}} 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

301 
} 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

302 

de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

303 
@manual{isabellesledgehammer, 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

304 
author = {Jasmin Christian Blanchette}, 
53647  305 
title = {Hammering Away: A User's Guide to {S}ledgehammer for {I}sabelle\slash {HOL}}, 
42215
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

306 
institution = TUM, 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

307 
note = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}} 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

308 
} 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

309 

36926  310 
@inproceedings{blanchettenipkow2010, 
311 
title = "Nitpick: A Counterexample Generator for HigherOrder Logic Based on a Relational Model Finder", 

33191  312 
author = "Jasmin Christian Blanchette and Tobias Nipkow", 
36926  313 
crossref = {itp2010}} 
314 

52805  315 
@unpublished{blanchetteetalwit, 
52829  316 
author = {J. C. Blanchette and A. Popescu and D. Traytel}, 
52805  317 
title = {Witnessing (Co)datatypes}, 
318 
year = 2013, 

319 
note = {\url{http://www21.in.tum.de/~traytel/papers/witness/wit.pdf}}} 

320 

46643
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

321 
@inproceedings{why3, 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

322 
author = {Fran\c{c}ois Bobot and JeanChristophe Filli\^atre and Claude March\'e and Andrei Paskevich}, 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

323 
title = {{Why3}: Shepherd Your Herd of Provers}, 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

324 
editor = "K. Rustan M. Leino and Micha\l{} Moskal", 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

325 
booktitle = {Boogie 2011}, 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

326 
pages = "5364", 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

327 
year = 2011 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

328 
} 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

329 

a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

330 
@inproceedings{altergo, 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

331 
author = {Fran\c{c}ois Bobot and Sylvain Conchon and Evelyne Contejean and St\'ephane Lescuyer}, 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

332 
title = {Implementing Polymorphism in {SMT} Solvers}, 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

333 
booktitle = {SMT '08}, 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

334 
pages = "15", 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

335 
publisher = "ACM", 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

336 
series = "ICPS", 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

337 
year = 2008, 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

338 
editor = {Clark Barrett and Leonardo de Moura}} 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

339 
% /BPR 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

340 
% and Domagoj Babic and Amit Goel 
a88bccd2b567
added support for AltErgo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents:
46286
diff
changeset

341 

36926  342 
@inproceedings{boehmenipkow2010, 
343 
author={Sascha B\"ohme and Tobias Nipkow}, 

344 
title={Sledgehammer: Judgement Day}, 

345 
booktitle={Automated Reasoning: IJCAR 2010}, 

346 
editor={J. Giesl and R. H\"ahnle}, 

347 
publisher=Springer, 

348 
series=LNCS, 

42964
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

349 
volume = 6173, 
bf45fd2488a2
document primitive support for LEOII and Satallax
blanchet
parents:
42940
diff
changeset

350 
pages = "107121", 
36926  351 
year=2010} 
33191  352 

6592  353 
@Article{boyer86, 
354 
author = {Robert Boyer and Ewing Lusk and William McCune and Ross 

355 
Overbeek and Mark Stickel and Lawrence Wos}, 

356 
title = {Set Theory in FirstOrder Logic: Clauses for {G\"{o}del's} 

357 
Axioms}, 

358 
journal = JAR, 

359 
year = 1986, 

360 
volume = 2, 

361 
number = 3, 

362 
pages = {287327}} 

363 

364 
@book{bm79, 

365 
author = {Robert S. Boyer and J Strother Moore}, 

366 
title = {A Computational Logic}, 

367 
publisher = {Academic Press}, 

368 
year = 1979} 

369 

370 
@book{bm88book, 

371 
author = {Robert S. Boyer and J Strother Moore}, 

372 
title = {A Computational Logic Handbook}, 

373 
publisher = {Academic Press}, 

374 
year = 1988} 

375 

44093  376 
@inproceedings{satallax, 
377 
author = "Chad E. Brown", 

378 
title = "Reducing HigherOrder Theorem Proving to a Sequence of {SAT} Problems", 

379 
booktitle = {Automated Deduction  CADE23}, 

380 
publisher = Springer, 

381 
series = LNCS, 

382 
volume = 6803, 

383 
pages = "147161", 

384 
editor = "Nikolaj Bj{\o}rner and Viorica SofronieStokkermans", 

385 
year = 2011} 

386 

6592  387 
@Article{debruijn72, 
388 
author = {N. G. de Bruijn}, 

389 
title = {Lambda Calculus Notation with Nameless Dummies, 

390 
a Tool for Automatic Formula Manipulation, 

391 
with Application to the {ChurchRosser Theorem}}, 

392 
journal = {Indag. Math.}, 

393 
volume = 34, 

394 
pages = {381392}, 

395 
year = 1972} 

396 

23187  397 
@InProceedings{bulwahnKN07, 
25093  398 
author = {Lukas Bulwahn and Alexander Krauss and Tobias Nipkow}, 
399 
title = {Finding Lexicographic Orders for Termination Proofs in {Isabelle/HOL}}, 

400 
crossref = {tphols2007}, 

401 
pages = {3853} 

402 
} 

23187  403 

28593  404 
@InProceedings{bulwahnetal:2008:imperative, 
33191  405 
author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent ErkÃ¶k and John Matthews}, 
28593  406 
title = {Imperative Functional Programming with {Isabelle/HOL}}, 
407 
crossref = {tphols2008}, 

408 
} 

409 
% pages = {3853} 

410 

11246  411 
@Article{ban89, 
412 
author = {M. Burrows and M. Abadi and R. M. Needham}, 

413 
title = {A Logic of Authentication}, 

414 
journal = PROYAL, 

415 
year = 1989, 

416 
volume = 426, 

417 
pages = {233271}} 

418 

6592  419 
%C 
420 

50130  421 
@PhdThesis{Chaiebthesis, 
422 
author = {Amine Chaieb}, 

423 
title = {Automated methods for formal proofs in simple arithmetics and algebra}, 

424 
school = {Technische Universit\"at M\"unchen}, 

425 
year = 2008, 

426 
note = {\url{http://www4.in.tum.de/~chaieb/pubs/pdf/diss.pdf}}} 

427 

39877  428 
@InProceedings{ChaiebWenzel:2007, 
429 
author = {Amine Chaieb and Makarius Wenzel}, 

430 
title = {Context aware Calculation and Deduction  

431 
Ring Equalities via {Gr\"obner Bases} in {Isabelle}}, 

432 
booktitle = {Towards Mechanized Mathematical Assistants (CALCULEMUS 2007)}, 

433 
editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger}, 

434 
series = LNAI, 

435 
volume = 4573, 

436 
year = 2007, 

437 
publisher = Springer 

438 
} 

439 

6592  440 
@TechReport{camilleri92, 
441 
author = {J. Camilleri and T. F. Melham}, 

442 
title = {Reasoning with Inductively Defined Relations in the 

443 
{HOL} Theorem Prover}, 

444 
institution = CUCL, 

445 
year = 1992, 

446 
number = 265, 

447 
month = Aug} 

448 

449 
@Book{charniak80, 

450 
author = {E. Charniak and C. K. Riesbeck and D. V. McDermott}, 

451 
title = {Artificial Intelligence Programming}, 

452 
publisher = {Lawrence Erlbaum Associates}, 

453 
year = 1980} 

454 

455 
@article{church40, 

456 
author = "Alonzo Church", 

457 
title = "A Formulation of the Simple Theory of Types", 

458 
journal = JSL, 

459 
year = 1940, 

460 
volume = 5, 

461 
pages = "5668"} 

462 

10191  463 
@book{ClarkeGPbook,author="Edmund Clarke and Orna Grumberg and Doron Peled", 
464 
title="Model Checking",publisher=MIT,year=1999} 

465 

6592  466 
@PhdThesis{coen92, 
467 
author = {Martin D. Coen}, 

468 
title = {Interactive Program Derivation}, 

469 
school = {University of Cambridge}, 

470 
note = {Computer Laboratory Technical Report 272}, 

471 
month = nov, 

472 
year = 1992} 

473 

474 
@book{constable86, 

475 
author = {R. L. Constable and others}, 

476 
title = {Implementing Mathematics with the Nuprl Proof 

54583  477 
Development System}, 
6592  478 
publisher = Prentice, 
479 
year = 1986} 

480 

481 
%D 

482 

6745  483 
@Book{daveypriestley, 
6592  484 
author = {B. A. Davey and H. A. Priestley}, 
485 
title = {Introduction to Lattices and Order}, 

486 
publisher = CUP, 

487 
year = 1990} 

488 

489 
@Book{devlin79, 

490 
author = {Keith J. Devlin}, 

491 
title = {Fundamentals of Contemporary Set Theory}, 

492 
publisher = {Springer}, 

493 
year = 1979} 

494 

495 
@book{dummett, 

496 
author = {Michael Dummett}, 

497 
title = {Elements of Intuitionism}, 

498 
year = 1977, 

499 
publisher = {Oxford University Press}} 

500 

40942  501 
@misc{yices, 
502 
author = {Bruno Dutertre and Leonardo de Moura}, 

503 
title = {The {Yices} {SMT} Solver}, 

42884  504 
howpublished = "\url{http://yices.csl.sri.com/toolpaper.pdf}", 
40942  505 
year = 2006} 
506 

6592  507 
@incollection{dybjer91, 
508 
author = {Peter Dybjer}, 

10186  509 
title = {Inductive Sets and Families in {MartinL{\"o}f's} Type 
54583  510 
Theory and Their SetTheoretic Semantics}, 
6592  511 
crossref = {huetplotkin91}, 
512 
pages = {280306}} 

513 

514 
@Article{dyckhoff, 

515 
author = {Roy Dyckhoff}, 

516 
title = {ContractionFree Sequent Calculi for Intuitionistic Logic}, 

517 
journal = JSL, 

518 
year = 1992, 

519 
volume = 57, 

520 
number = 3, 

521 
pages = {795807}} 

522 

523 
%F 

524 

6613
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

525 
@Article{IMPS, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

526 
author = {William M. Farmer and Joshua D. Guttman and F. Javier 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

527 
Thayer}, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

528 
title = {{IMPS}: An Interactive Mathematical Proof System}, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

529 
journal = JAR, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

530 
volume = 11, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

531 
number = 2, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

532 
year = 1993, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

533 
pages = {213248}} 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

534 

6592  535 
@InProceedings{felty91a, 
536 
Author = {Amy Felty}, 

537 
Title = {A Logic Program for Transforming Sequent Proofs to Natural 

54583  538 
Deduction Proofs}, 
6592  539 
crossref = {extensions91}, 
540 
pages = {157178}} 

541 

10796  542 
@Article{fleuriotjcm, 
543 
author = {Jacques Fleuriot and Lawrence C. Paulson}, 

544 
title = {Mechanizing Nonstandard Real Analysis}, 

545 
journal = {LMS Journal of Computation and Mathematics}, 

546 
year = 2000, 

547 
volume = 3, 

548 
pages = {140190}, 

549 
note = {\url{http://www.lms.ac.uk/jcm/3/lms1999027/}} 

550 
} 

551 

6592  552 
@TechReport{frost93, 
553 
author = {Jacob Frost}, 

554 
title = {A Case Study of Coinduction in {Isabelle HOL}}, 

555 
institution = CUCL, 

556 
number = 308, 

557 
year = 1993, 

558 
month = Aug} 

559 

560 
%revised version of frost93 

561 
@TechReport{frost95, 

562 
author = {Jacob Frost}, 

563 
title = {A Case Study of Coinduction in {Isabelle}}, 

564 
institution = CUCL, 

565 
number = 359, 

566 
year = 1995, 

567 
month = Feb} 

568 

569 
@inproceedings{OBJ, 

570 
author = {K. Futatsugi and J.A. Goguen and JeanPierre Jouannaud 

54583  571 
and J. Meseguer}, 
6592  572 
title = {Principles of {OBJ2}}, 
54583  573 
booktitle = POPL, 
6592  574 
year = 1985, 
575 
pages = {5266}} 

576 

577 
%G 

578 

579 
@book{gallier86, 

580 
author = {J. H. Gallier}, 

54583  581 
title = {Logic for Computer Science: 
6592  582 
Foundations of Automatic Theorem Proving}, 
583 
year = 1986, 

584 
publisher = {Harper \& Row}} 

585 

586 
@Book{galton90, 

587 
author = {Antony Galton}, 

588 
title = {Logic for Information Technology}, 

589 
publisher = {Wiley}, 

590 
year = 1990} 

591 

20506  592 
@Article{Gentzen:1935, 
593 
author = {G. Gentzen}, 

594 
title = {Untersuchungen {\"u}ber das logische {S}chlie{\ss}en}, 

595 
journal = {Math. Zeitschrift}, 

596 
year = 1935 

597 
} 

598 

6592  599 
@InProceedings{gimenezcodifying, 
600 
author = {Eduardo Gim{\'e}nez}, 

601 
title = {Codifying Guarded Definitions with Recursive Schemes}, 

602 
crossref = {types94}, 

603 
pages = {3959} 

604 
} 

605 

9816  606 
@book{girard89, 
607 
author = {JeanYves Girard}, 

608 
title = {Proofs and Types}, 

609 
year = 1989, 

54583  610 
publisher = CUP, 
611 
note = {Translated by Yves Lafont and Paul Taylor}} 

9816  612 

6592  613 
@Book{mgordonhol, 
11205  614 
editor = {M. J. C. Gordon and T. F. Melham}, 
42907
dfd4ef8e73f6
updated and reunified HOL typedef, with some live examples;
wenzelm
parents:
42884
diff
changeset

615 
title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic}, 
6592  616 
publisher = CUP, 
617 
year = 1993} 

618 

619 
@book{mgordon79, 

620 
author = {Michael J. C. Gordon and Robin Milner and Christopher P. 

621 
Wadsworth}, 

622 
title = {Edinburgh {LCF}: A Mechanised Logic of Computation}, 

623 
year = 1979, 

624 
publisher = {Springer}, 

625 
series = {LNCS 78}} 

626 

6607  627 
@inproceedings{GunterHOL92,author={Elsa L. Gunter}, 
628 
title={Why we can't have {SML} style datatype declarations in {HOL}}, 

629 
booktitle={Higher Order Logic Theorem Proving and its Applications: Proc.\ 

630 
IFIP TC10/WG10.2 Intl. Workshop, 1992}, 

631 
editor={L.J.M. Claesen and M.J.C. Gordon}, 

632 
publisher=NH,year=1993,pages={561568}} 

633 

6592  634 
@InProceedings{guntertrees, 
635 
author = {Elsa L. Gunter}, 

636 
title = {A Broader Class of Trees for Recursive Type Definitions for 

637 
{HOL}}, 

638 
crossref = {hug93}, 

639 
pages = {141154}} 

640 

641 
%H 

642 

53125  643 
@inproceedings{HaftmannKrausKuncarNipkow:2013:data_refinement, 
644 
author = {Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow}, 

645 
title = {Data Refinement in Isabelle/HOL}, 

646 
booktitle = {Interactive Theorem Proving (ITP 2013)}, 

647 
pages = {100115}, 

648 
year = 2013, 

649 
publisher = Springer, 

650 
series = {Lecture Notes in Computer Science}, 

651 
volume = {7998}, 

652 
editor = {S. Blazy and C. PaulinMohring and D. Pichardie} 

24193  653 
} 
654 

37429  655 
@inproceedings{HaftmannNipkow:2010:code, 
656 
author = {Florian Haftmann and Tobias Nipkow}, 

657 
title = {Code Generation via HigherOrder Rewrite Systems}, 

658 
booktitle = {Functional and Logic Programming: 10th International Symposium: FLOPS 2010}, 

659 
year = 2010, 

38437  660 
publisher = Springer, 
661 
series = LNCS, 

37429  662 
editor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal}, 
38437  663 
volume = 6009 
23956  664 
} 
665 

53125  666 
@InProceedings{HaftmannWenzel:2006:classes, 
667 
author = {Florian Haftmann and Makarius Wenzel}, 

668 
title = {Constructive Type Classes in {Isabelle}}, 

669 
editor = {T. Altenkirch and C. McBride}, 

670 
booktitle = {Types for Proofs and Programs, TYPES 2006}, 

671 
publisher = {Springer}, 

672 
series = {LNCS}, 

673 
volume = {4502}, 

674 
year = {2007} 

675 
} 

676 

30115  677 
@InProceedings{HaftmannWenzel:2009, 
678 
author = {Florian Haftmann and Makarius Wenzel}, 

679 
title = {Local theory specifications in {Isabelle/Isar}}, 

680 
editor = {Stefano Berardi and Ferruccio Damiani and de Liguoro, Ugo}, 

681 
booktitle = {Types for Proofs and Programs, TYPES 2008}, 

682 
publisher = {Springer}, 

683 
series = {LNCS}, 

32572  684 
volume = {5497}, 
30115  685 
year = {2009} 
686 
} 

687 

45258  688 
@inproceedings{hindleymilner, 
689 
author = {L. Damas and H. Milner}, 

690 
title = {Principal type schemes for functional programs}, 

691 
booktitle = {ACM Symp. Principles of Programming Languages}, 

692 
year = 1982 

693 
} 

694 

22290  695 
@manual{isabelleclasses, 
24193  696 
author = {Florian Haftmann}, 
697 
title = {Haskellstyle type classes with {Isabelle}/{Isar}}, 

698 
institution = TUM, 

699 
note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}} 

700 
} 

22290  701 

702 
@manual{isabellecodegen, 

24193  703 
author = {Florian Haftmann}, 
704 
title = {Code generation from Isabelle theories}, 

705 
institution = TUM, 

706 
note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}} 

707 
} 

22290  708 

6592  709 
@Book{halmos60, 
710 
author = {Paul R. Halmos}, 

711 
title = {Naive Set Theory}, 

712 
publisher = {Van Nostrand}, 

713 
year = 1960} 

714 

11207  715 
@book{HarelKTDL,author={David Harel and Dexter Kozen and Jerzy Tiuryn}, 
716 
title={Dynamic Logic},publisher=MIT,year=2000} 

717 

6592  718 
@Book{hennessy90, 
719 
author = {Matthew Hennessy}, 

720 
title = {The Semantics of Programming Languages: An Elementary 

721 
Introduction Using Structural Operational Semantics}, 

722 
publisher = {Wiley}, 

723 
year = 1990} 

724 

42940  725 
@article{waldmeister, 
726 
author = {Thomas Hillenbrand and Arnim Buch and Rolan Vogt and Bernd L\"ochner}, 

727 
title = "Waldmeister: HighPerformance Equational Deduction", 

728 
journal = JAR, 

729 
volume = 18, 

730 
number = 2, 

731 
pages = {265270}, 

732 
year = 1997} 

733 

10244  734 
@book{HopcroftUllman,author={John E. Hopcroft and Jeffrey D. Ullman}, 
735 
title={Introduction to Automata Theory, Languages, and Computation.}, 

736 
publisher={AddisonWesley},year=1979} 

737 

6592  738 
@Article{haskellreport, 
739 
author = {Paul Hudak and Simon Peyton Jones and Philip Wadler}, 

740 
title = {Report on the Programming Language {Haskell}: A 

741 
Nonstrict, Purely Functional Language}, 

742 
journal = SIGPLAN, 

743 
year = 1992, 

744 
volume = 27, 

745 
number = 5, 

746 
month = May, 

747 
note = {Version 1.2}} 

748 

749 
@Article{haskelltutorial, 

750 
author = {Paul Hudak and Joseph H. Fasel}, 

751 
title = {A Gentle Introduction to {Haskell}}, 

752 
journal = SIGPLAN, 

753 
year = 1992, 

754 
volume = 27, 

755 
number = 5, 

756 
month = May} 

757 

42884  758 
@inproceedings{sine, 
759 
author = "Kry\v{s}tof Hoder and Andrei Voronkov", 

760 
title = "Sine Qua Non for Large Theory Reasoning", 

761 
booktitle = {Automated Deduction  CADE23}, 

762 
publisher = Springer, 

763 
series = LNCS, 

44093  764 
volume = 6803, 
765 
pages = "299314", 

42884  766 
editor = "Nikolaj Bj{\o}rner and Viorica SofronieStokkermans", 
44093  767 
year = 2011} 
38602  768 

11209  769 
@book{HudakHaskell,author={Paul Hudak}, 
770 
title={The Haskell School of Expression},publisher=CUP,year=2000} 

771 

6592  772 
@article{huet75, 
773 
author = {G. P. Huet}, 

774 
title = {A Unification Algorithm for Typed $\lambda$Calculus}, 

775 
journal = TCS, 

776 
volume = 1, 

777 
year = 1975, 

778 
pages = {2757}} 

779 

780 
@article{huet78, 

781 
author = {G. P. Huet and B. Lang}, 

54583  782 
title = {Proving and Applying Program Transformations Expressed with 
6592  783 
SecondOrder Patterns}, 
784 
journal = acta, 

785 
volume = 11, 

54583  786 
year = 1978, 
6592  787 
pages = {3155}} 
788 

789 
@inproceedings{huet88, 

10186  790 
author = {G{\'e}rard Huet}, 
6592  791 
title = {Induction Principles Formalized in the {Calculus of 
54583  792 
Constructions}}, 
6592  793 
booktitle = {Programming of Future Generation Computers}, 
794 
editor = {K. Fuchi and M. Nivat}, 

795 
year = 1988, 

54583  796 
pages = {205216}, 
6592  797 
publisher = {Elsevier}} 
798 

54334
409d7f7247f4
update documentation of Lifting/Transfer and Quotient
kuncar
parents:
53769
diff
changeset

799 
@inproceedings{HuffmanKuncar:2013:lifting_transfer, 
409d7f7247f4
update documentation of Lifting/Transfer and Quotient
kuncar
parents:
53769
diff
changeset

800 
author = {Brian Huffman and Ond\v{r}ej Kun\v{c}ar}, 
409d7f7247f4
update documentation of Lifting/Transfer and Quotient
kuncar
parents:
53769
diff
changeset

801 
title = {{Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL}}, 
409d7f7247f4
update documentation of Lifting/Transfer and Quotient
kuncar
parents:
53769
diff
changeset

802 
booktitle = {Certified Programs and Proofs (CPP 2013)}, 
409d7f7247f4
update documentation of Lifting/Transfer and Quotient
kuncar
parents:
53769
diff
changeset

803 
year = 2013, 
409d7f7247f4
update documentation of Lifting/Transfer and Quotient
kuncar
parents:
53769
diff
changeset

804 
publisher = Springer, 
409d7f7247f4
update documentation of Lifting/Transfer and Quotient
kuncar
parents:
53769
diff
changeset

805 
series = {Lecture Notes in Computer Science}, 
409d7f7247f4
update documentation of Lifting/Transfer and Quotient
kuncar
parents:
53769
diff
changeset

806 
volume = {8307}, 
409d7f7247f4
update documentation of Lifting/Transfer and Quotient
kuncar
parents:
53769
diff
changeset

807 
} 
409d7f7247f4
update documentation of Lifting/Transfer and Quotient
kuncar
parents:
53769
diff
changeset

808 

10186  809 
@Book{HuthRyanbook, 
810 
author = {Michael Huth and Mark Ryan}, 

811 
title = {Logic in Computer Science. Modelling and reasoning about systems}, 

812 
publisher = CUP, 

813 
year = 2000} 

814 

7041  815 
@InProceedings{Harrison:1996:MizarHOL, 
816 
author = {J. Harrison}, 

817 
title = {A {Mizar} Mode for {HOL}}, 

818 
pages = {203220}, 

819 
crossref = {tphols96}} 

820 

36926  821 
@misc{metis, 
822 
author = "Joe Hurd", 

823 
title = "Metis Theorem Prover", 

824 
note = "\url{http://www.gilith.com/software/metis/}"} 

825 

22290  826 
%J 
827 

828 
@article{haskellrevisedreport, 

829 
author = {Simon {Peyton Jones} and others}, 

830 
title = {The {Haskell} 98 Language and Libraries: The Revised Report}, 

831 
journal = {Journal of Functional Programming}, 

832 
volume = 13, 

833 
number = 1, 

834 
pages = {0255}, 

835 
month = {Jan}, 

836 
year = 2003, 

837 
note = {\url{http://www.haskell.org/definition/}}} 

838 

33191  839 
@book{jackson2006, 
840 
author = "Daniel Jackson", 

841 
title = "Software Abstractions: Logic, Language, and Analysis", 

842 
publisher = MIT, 

843 
year = 2006} 

844 

6592  845 
%K 
846 

6670  847 
@InProceedings{kammuellerlocales, 
54583  848 
author = {Florian Kamm{\"u}ller and Markus Wenzel and 
6670  849 
Lawrence C. Paulson}, 
850 
title = {Locales: A Sectioning Concept for {Isabelle}}, 

851 
crossref = {tphols99}} 

852 

8284  853 
@book{Knuth375, 
854 
author={Donald E. Knuth}, 

855 
title={The Art of Computer Programming, Volume 3: Sorting and Searching}, 

856 
publisher={AddisonWesley}, 

857 
year=1975} 

858 

859 
@Article{korf85, 

860 
author = {R. E. Korf}, 

861 
title = {DepthFirst IterativeDeepening: an Optimal Admissible 

862 
Tree Search}, 

863 
journal = AI, 

864 
year = 1985, 

865 
volume = 27, 

866 
pages = {97109}} 

6607  867 

45339  868 
@inproceedings{korovin2009, 
869 
title = "InstantiationBased Automated Reasoning: From Theory to Practice", 

870 
author = "Konstantin Korovin", 

871 
editor = "Renate A. Schmidt", 

872 
booktitle = {Automated Deduction  CADE22}, 

873 
series = "LNAI", 

874 
volume = {5663}, 

875 
pages = "163166", 

876 
year = 2009, 

877 
publisher = "Springer"} 

878 

879 
@inproceedings{korovinsticksel2010, 

880 
author = {Konstantin Korovin and 

881 
Christoph Sticksel}, 

882 
title = {{iP}rover{E}q: An InstantiationBased Theorem Prover with Equality}, 

883 
pages = {196202}, 

884 
booktitle={Automated Reasoning: IJCAR 2010}, 

885 
editor={J. Giesl and R. H\"ahnle}, 

886 
publisher = Springer, 

887 
series = LNCS, 

888 
volume = 6173, 

889 
year = 2010} 

890 

23187  891 
@InProceedings{krauss2006, 
892 
author = {Alexander Krauss}, 

893 
title = {Partial Recursive Functions in {HigherOrder Logic}}, 

894 
crossref = {ijcar2006}, 

895 
pages = {589603}} 

896 

33856  897 
@PhdThesis{krauss_phd, 
898 
author = {Alexander Krauss}, 

899 
title = {Automating Recursive Definitions and Termination Proofs in HigherOrder Logic}, 

900 
school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}, 

901 
year = {2009}, 

902 
address = {Germany} 

903 
} 

904 

24524  905 
@manual{isabellefunction, 
906 
author = {Alexander Krauss}, 

907 
title = {Defining Recursive Functions in {Isabelle/HOL}}, 

908 
institution = TUM, 

25280  909 
note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}} 
24524  910 
} 
911 

6592  912 
@Book{kunen80, 
913 
author = {Kenneth Kunen}, 

914 
title = {Set Theory: An Introduction to Independence Proofs}, 

915 
publisher = NH, 

916 
year = 1980} 

917 

11246  918 
%L 
919 

22290  920 
@manual{OCaml, 
921 
author = {Xavier Leroy and others}, 

922 
title = {The Objective Caml system  Documentation and user's manual}, 

923 
note = {\url{http://caml.inria.fr/pub/docs/manualocaml/}}} 

924 

52078  925 
@misc{agsyHOL, 
926 
author = "Fredrik Lindblad", 

927 
title = "{agsyHOL}", 

928 
note = "\url{https://github.com/frelindb/agsyHOL}"} 

929 

38602  930 
@incollection{lochbihler2010, 
54146  931 
title = "Coinductive", 
38602  932 
author = "Andreas Lochbihler", 
933 
booktitle = "The Archive of Formal Proofs", 

934 
editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson", 

935 
publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}", 

936 
month = "Feb.", 

937 
year = 2010} 

938 

43579  939 
@book{loveland78, 
940 
author = "D. W. Loveland", 

941 
title = "Automated Theorem Proving: A Logical Basis", 

942 
year = 1978, 

943 
publisher = "NorthHolland Publishing Co."} 

944 

11246  945 
@InProceedings{lowefdr, 
946 
author = {Gavin Lowe}, 

947 
title = {Breaking and Fixing the {Needham}{Schroeder} PublicKey 

948 
Protocol using {CSP} and {FDR}}, 

54583  949 
booktitle = {Tools and Algorithms for the Construction and Analysis 
11246  950 
of Systems: second international workshop, TACAS '96}, 
951 
editor = {T. Margaria and B. Steffen}, 

952 
series = {LNCS 1055}, 

953 
year = 1996, 

954 
publisher = {Springer}, 

955 
pages = {147166}} 

956 

6592  957 
%M 
958 

959 
@Article{mw81, 

960 
author = {Zohar Manna and Richard Waldinger}, 

961 
title = {Deductive Synthesis of the Unification Algorithm}, 

962 
journal = SCP, 

963 
year = 1981, 

964 
volume = 1, 

965 
number = 1, 

966 
pages = {548}} 

967 

968 
@InProceedings{martinnipkow, 

969 
author = {Ursula Martin and Tobias Nipkow}, 

970 
title = {Ordered Rewriting and Confluence}, 

971 
crossref = {cade10}, 

972 
pages = {366380}} 

973 

974 
@book{martinlof84, 

10186  975 
author = {Per MartinL{\"o}f}, 
6592  976 
title = {Intuitionistic type theory}, 
977 
year = 1984, 

978 
publisher = {Bibliopolis}} 

979 

980 
@incollection{melham89, 

981 
author = {Thomas F. Melham}, 

982 
title = {Automating Recursive Type Definitions in Higher Order 

54583  983 
Logic}, 
6592  984 
pages = {341386}, 
985 
crossref = {birtwistle89}} 

986 

29728  987 
@Article{Miller:1991, 
988 
author = {Dale Miller}, 

989 
title = {A Logic Programming Language with LambdaAbstraction, Function Variables, 

990 
and Simple Unification}, 

991 
journal = {Journal of Logic and Computation}, 

992 
year = 1991, 

993 
volume = 1, 

994 
number = 4 

995 
} 

996 

6592  997 
@Article{millermixed, 
998 
Author = {Dale Miller}, 

999 
Title = {Unification Under a Mixed Prefix}, 

1000 
journal = JSC, 

1001 
volume = 14, 

1002 
number = 4, 

1003 
pages = {321358}, 

1004 
Year = 1992} 

1005 

1006 
@Article{milner78, 

1007 
author = {Robin Milner}, 

1008 
title = {A Theory of Type Polymorphism in Programming}, 

1009 
journal = "J. Comp.\ Sys.\ Sci.", 

1010 
year = 1978, 

1011 
volume = 17, 

1012 
pages = {348375}} 

1013 

1014 
@TechReport{milnerind, 

1015 
author = {Robin Milner}, 

1016 
title = {How to Derive Inductions in {LCF}}, 

1017 
institution = Edinburgh, 

1018 
year = 1980, 

1019 
type = {note}} 

1020 

1021 
@Article{milnercoind, 

1022 
author = {Robin Milner and Mads Tofte}, 

1023 
title = {Coinduction in Relational Semantics}, 

1024 
journal = TCS, 

1025 
year = 1991, 

1026 
volume = 87, 

1027 
pages = {209220}} 

1028 

1029 
@Book{milner89, 

1030 
author = {Robin Milner}, 

1031 
title = {Communication and Concurrency}, 

1032 
publisher = Prentice, 

1033 
year = 1989} 

1034 

10970  1035 
@book{SML,author="Robin Milner and Mads Tofte and Robert Harper", 
1036 
title="The Definition of Standard ML",publisher=MIT,year=1990} 

1037 

6592  1038 
@PhdThesis{monahan84, 
1039 
author = {Brian Q. Monahan}, 

1040 
title = {Data Type Proofs using Edinburgh {LCF}}, 

1041 
school = {University of Edinburgh}, 

1042 
year = 1984} 

1043 

6607  1044 
@article{MuellerNvOS99, 
1045 
author= 

11564  1046 
{Olaf M{\"u}ller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch}, 
11197  1047 
title={{HOLCF = HOL + LCF}},journal=JFP,year=1999,volume=9,pages={191223}} 
6607  1048 

9599  1049 
@Manual{Muzalewski:Mizar, 
1050 
title = {An Outline of {PC} {Mizar}}, 

1051 
author = {Micha{\l} Muzalewski}, 

1052 
organization = {Fondation of Logic, Mathematics and Informatics 

1053 
 Mizar Users Group}, 

1054 
year = 1993, 

1055 
note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz}} 

1056 
} 

1057 

6592  1058 
%N 
1059 

1060 
@InProceedings{NaraschewskiWTPHOLs98, 

1061 
author = {Wolfgang Naraschewski and Markus Wenzel}, 

54583  1062 
title = 
7041  1063 
{ObjectOriented Verification based on Record Subtyping in 
1064 
HigherOrder Logic}, 

1065 
crossref = {tphols98}} 

6592  1066 

1067 
@inproceedings{nazarethnipkow, 

1068 
author = {Dieter Nazareth and Tobias Nipkow}, 

1069 
title = {Formal Verification of Algorithm {W}: The Monomorphic Case}, 

1070 
crossref = {tphols96}, 

1071 
pages = {331345}, 

1072 
year = 1996} 

1073 

11246  1074 
@Article{needhamschroeder, 
1075 
author = "Roger M. Needham and Michael D. Schroeder", 

1076 
title = "Using Encryption for Authentication in Large Networks 

1077 
of Computers", 

1078 
journal = cacm, 

1079 
volume = 21, 

1080 
number = 12, 

1081 
pages = "993999", 

1082 
month = dec, 

1083 
year = 1978} 

1084 

6592  1085 
@inproceedings{nipkowW, 
1086 
author = {Wolfgang Naraschewski and Tobias Nipkow}, 

1087 
title = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}}, 

1088 
booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96}, 

10186  1089 
editor = {E. Gim{\'e}nez and C. PaulinMohring}, 
6592  1090 
publisher = Springer, 
1091 
series = LNCS, 

1092 
volume = 1512, 

1093 
pages = {317332}, 

1094 
year = 1998} 

1095 

8892  1096 
@InCollection{nipkowsorts93, 
1097 
author = {T. Nipkow}, 

1098 
title = {OrderSorted Polymorphism in {Isabelle}}, 

1099 
booktitle = {Logical Environments}, 

1100 
publisher = CUP, 

1101 
year = 1993, 

1102 
editor = {G. Huet and G. Plotkin}, 

1103 
pages = {164188} 

1104 
} 

1105 

1106 
@Misc{nipkowtypes93, 

1107 
author = {Tobias Nipkow}, 

1108 
title = {Axiomatic Type Classes (in {I}sabelle)}, 

1109 
howpublished = {Presentation at the workshop \emph{Types for Proof and Programs}, Nijmegen}, 

1110 
year = 1993 

1111 
} 

1112 

6592  1113 
@inproceedings{NipkowCR, 
1114 
author = {Tobias Nipkow}, 

1115 
title = {More {ChurchRosser} Proofs (in {Isabelle/HOL})}, 

1116 
booktitle = {Automated Deduction  CADE13}, 

1117 
editor = {M. McRobbie and J.K. Slaney}, 

1118 
publisher = Springer, 

1119 
series = LNCS, 

1120 
volume = 1104, 

1121 
pages = {733747}, 

1122 
year = 1996} 

1123 

1124 
% WAS NipkowLICS93 

1125 
@InProceedings{nipkowpatterns, 

1126 
title = {Functional Unification of HigherOrder Patterns}, 

1127 
author = {Tobias Nipkow}, 

1128 
pages = {6474}, 

1129 
crossref = {lics8}, 

6745  1130 
url = {\url{ftp://ftp.informatik.tumuenchen.de/local/lehrstuhl/nipkow/lics93.html}}, 
6592  1131 
keywords = {unification}} 
1132 

1133 
@article{nipkowIMP, 

1134 
author = {Tobias Nipkow}, 

1135 
title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook}, 

1136 
journal = FAC, 

1137 
volume = 10, 

1138 
pages = {171186}, 

1139 
year = 1998} 

1140 

15429  1141 
@inproceedings{NipkowTYPES02, 
1142 
author = {Tobias Nipkow}, 

1143 
title = {{Structured Proofs in Isar/HOL}}, 

1144 
booktitle = {Types for Proofs and Programs (TYPES 2002)}, 

1145 
editor = {H. Geuvers and F. Wiedijk}, 

1146 
year = 2003, 

1147 
publisher = Springer, 

1148 
series = LNCS, 

1149 
volume = 2646, 

1150 
pages = {259278}} 

1151 

6607  1152 
@manual{isabelleHOL, 
1153 
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, 

1154 
title = {{Isabelle}'s Logics: {HOL}}, 

10186  1155 
institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t 
1156 
M{\"u}nchen and Computer Laboratory, University of Cambridge}, 

8892  1157 
note = {\url{http://isabelle.in.tum.de/doc/logicsHOL.pdf}}} 
6607  1158 

6592  1159 
@article{nipkowprehofer, 
1160 
author = {Tobias Nipkow and Christian Prehofer}, 

1161 
title = {Type Reconstruction for Type Classes}, 

1162 
journal = JFP, 

1163 
volume = 5, 

1164 
number = 2, 

1165 
year = 1995, 

1166 
pages = {201224}} 

1167 

23956  1168 
@InProceedings{NipkowPrehofer:1993, 
1169 
author = {T. Nipkow and C. Prehofer}, 

1170 
title = {Type checking type classes}, 

1171 
booktitle = {ACM Symp.\ Principles of Programming Languages}, 

1172 
year = 1993 

1173 
} 

1174 

14147  1175 
@Book{isatutorial, 
1176 
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, 

33191  1177 
title = {Isabelle/{HOL}: A Proof Assistant for HigherOrder Logic}, 
1178 
publisher = Springer, 

14147  1179 
year = 2002, 
33191  1180 
series = LNCS, 
1181 
volume = 2283} 

14147  1182 

6592  1183 
@Article{noel, 
1184 
author = {Philippe No{\"e}l}, 

1185 
title = {Experimenting with {Isabelle} in {ZF} Set Theory}, 

1186 
journal = JAR, 

1187 
volume = 10, 

1188 
number = 1, 

1189 
pages = {1558}, 

1190 
year = 1993} 

1191 

1192 
@book{nordstrom90, 

10186  1193 
author = {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith}, 
1194 
title = {Programming in {MartinL{\"o}f}'s Type Theory. An 

54583  1195 
Introduction}, 
1196 
publisher = {Oxford University Press}, 

6592  1197 
year = 1990} 
1198 

1199 
%O 

1200 

38814  1201 
@TechReport{scalaoverviewtechreport, 
1202 
author = {Martin Odersky and al.}, 

1203 
title = {An Overview of the Scala Programming Language}, 

1204 
institution = {EPFL Lausanne, Switzerland}, 

1205 
year = 2004, 

1206 
number = {IC/2004/64} 

1207 
} 

1208 

46286  1209 
@Article{Oppen:1980, 
1210 
author = {D. C. Oppen}, 

1211 
title = {Pretty Printing}, 

1212 
journal = {ACM Transactions on Programming Languages and Systems}, 

1213 
year = 1980, 

1214 
volume = 2, 

1215 
number = 4} 

1216 

6592  1217 
@Manual{pvslanguage, 
1218 
title = {The {PVS} specification language}, 

1219 
author = {S. Owre and N. Shankar and J. M. Rushby}, 

1220 
organization = {Computer Science Laboratory, SRI International}, 

1221 
address = {Menlo Park, CA}, 

6745  1222 
note = {Beta release}, 
6592  1223 
year = 1993, 
1224 
month = apr, 

6619  1225 
url = {\url{http://www.csl.sri.com/reports/pvslanguage.dvi.Z}}} 
6592  1226 

1227 
%P 

1228 

1229 
% replaces paulin92 

1230 
@InProceedings{paulintlca, 

1231 
author = {Christine PaulinMohring}, 

1232 
title = {Inductive Definitions in the System {Coq}: Rules and 

1233 
Properties}, 

1234 
crossref = {tlca93}, 

1235 
pages = {328345}} 

1236 

50122  1237 
@Article{paulson:1983, 
1238 
author = {L. C. Paulson}, 

1239 
title = {A higherorder implementation of rewriting}, 

1240 
journal = {Science of Computer Programming}, 

1241 
year = 1983, 

1242 
volume = 3, 

1243 
pages = {119149}, 

1244 
note = {\url{http://www.cl.cam.ac.uk/~lp15/papers/Reports/TR035lcprewriting.pdf}}} 

1245 

6592  1246 
@InProceedings{paulsonCADE, 
1247 
author = {Lawrence C. Paulson}, 

1248 
title = {A Fixedpoint Approach to Implementing (Co)Inductive 

1249 
Definitions}, 

1250 
pages = {148161}, 

1251 
crossref = {cade12}} 

1252 

1253 
@InProceedings{paulsonCOLOG, 

1254 
author = {Lawrence C. Paulson}, 

1255 
title = {A Formulation of the Simple Theory of Types (for 

54583  1256 
{Isabelle})}, 
6592  1257 
pages = {246274}, 
1258 
crossref = {colog88}, 

6619  1259 
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175lcpsimple.dvi.gz}}} 
6592  1260 

1261 
@Article{paulsoncoind, 

1262 
author = {Lawrence C. Paulson}, 

1263 
title = {Mechanizing Coinduction and Corecursion in HigherOrder 

1264 
Logic}, 

1265 
journal = JLC, 

1266 
year = 1997, 

1267 
volume = 7, 

1268 
number = 2, 

1269 
month = mar, 

1270 
pages = {175204}} 

1271 

12616  1272 
@manual{isabelleintro, 
1273 
author = {Lawrence C. Paulson}, 

39852  1274 
title = {Old Introduction to {Isabelle}}, 
12616  1275 
institution = CUCL, 
1276 
note = {\url{http://isabelle.in.tum.de/doc/intro.pdf}}} 

1277 

1278 
@manual{isabellelogics, 

1279 
author = {Lawrence C. Paulson}, 

1280 
title = {{Isabelle's} Logics}, 

1281 
institution = CUCL, 

1282 
note = {\url{http://isabelle.in.tum.de/doc/logics.pdf}}} 

1283 

6613
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

1284 
@manual{isabelleref, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

1285 
author = {Lawrence C. Paulson}, 
39852  1286 
title = {The Old {Isabelle} Reference Manual}, 
8892  1287 
institution = CUCL, 
1288 
note = {\url{http://isabelle.in.tum.de/doc/ref.pdf}}} 

6607  1289 

1290 
@manual{isabelleZF, 

6592  1291 
author = {Lawrence C. Paulson}, 
1292 
title = {{Isabelle}'s Logics: {FOL} and {ZF}}, 

8892  1293 
institution = CUCL, 
1294 
note = {\url{http://isabelle.in.tum.de/doc/logicsZF.pdf}}} 

6592  1295 

1296 
@article{paulsonfound, 

1297 
author = {Lawrence C. Paulson}, 

1298 
title = {The Foundation of a Generic Theorem Prover}, 

1299 
journal = JAR, 

1300 
volume = 5, 

1301 
number = 3, 

1302 
pages = {363397}, 

1303 
year = 1989, 

6619  1304 
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130lcpgenerictheoremprover.dvi.gz}}} 
6592  1305 

1306 
%replaces paulsonfinal 

1307 
@Article{paulsonmscs, 

1308 
author = {Lawrence C. Paulson}, 

54583  1309 
title = {Final Coalgebras as Greatest Fixed Points 
7991  1310 
in {ZF} Set Theory}, 
6592  1311 
journal = {Mathematical Structures in Computer Science}, 
1312 
year = 1999, 

1313 
volume = 9, 

23505  1314 
number = 5, 
1315 
pages = {545567}} 

6592  1316 

1317 
@InCollection{paulsongeneric, 

1318 
author = {Lawrence C. Paulson}, 

1319 
title = {Generic Automatic Proof Tools}, 

1320 
crossref = {wosfest}, 

1321 
chapter = 3} 

1322 

1323 
@Article{paulsongr, 

1324 
author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski}, 

1325 
title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of 

1326 
Choice}, 

1327 
journal = JAR, 

1328 
year = 1996, 

1329 
volume = 17, 

1330 
number = 3, 

1331 
month = dec, 

1332 
pages = {291323}} 

1333 

14210  1334 
@InCollection{paulsonfixedptmilner, 
1335 
author = {Lawrence C. Paulson}, 

1336 
title = {A Fixedpoint Approach to (Co)inductive and 

1337 
(Co)datatype Definitions}, 

1338 
pages = {187211}, 

1339 
crossref = {milnerfest}} 

1340 

1341 
@book{milnerfest, 

54583  1342 
title = {Proof, Language, and Interaction: 
14210  1343 
Essays in Honor of {Robin Milner}}, 
54583  1344 
booktitle = {Proof, Language, and Interaction: 
14210  1345 
Essays in Honor of {Robin Milner}}, 
33191  1346 
publisher = MIT, 
14210  1347 
year = 2000, 
1348 
editor = {Gordon Plotkin and Colin Stirling and Mads Tofte}} 

1349 

6592  1350 
@InCollection{paulsonhandbook, 
1351 
author = {Lawrence C. Paulson}, 

1352 
title = {Designing a Theorem Prover}, 

1353 
crossref = {handbklics2}, 

1354 
pages = {415475}} 

1355 

1356 
@Book{paulsonisabook, 

1357 
author = {Lawrence C. Paulson}, 

1358 
title = {Isabelle: A Generic Theorem Prover}, 

1359 
publisher = {Springer}, 

1360 
year = 1994, 

1361 
note = {LNCS 828}} 

1362 

12878  1363 
@Book{isabelleholbook, 
1364 
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, 

1365 
title = {Isabelle/HOL  A Proof Assistant for HigherOrder Logic}, 

1366 
publisher = {Springer}, 

1367 
year = 2002, 

1368 
note = {LNCS 2283}} 

1369 

6592  1370 
@InCollection{paulsonmarkt, 
1371 
author = {Lawrence C. Paulson}, 

1372 
title = {Tool Support for Logics of Programs}, 

1373 
booktitle = {Mathematical Methods in Program Development: 

1374 
Summer School Marktoberdorf 1996}, 

1375 
publisher = {Springer}, 

1376 
pages = {461498}, 

1377 
year = {Published 1997}, 

1378 
editor = {Manfred Broy}, 

1379 
series = {NATO ASI Series F}} 

1380 

1381 
%replaces PaulsonML and paulson91 

1382 
@book{paulsonml2, 

1383 
author = {Lawrence C. Paulson}, 

1384 
title = {{ML} for the Working Programmer}, 

1385 
year = 1996, 

1386 
edition = {2nd}, 

1387 
publisher = CUP} 

1388 

1389 
@article{paulsonnatural, 

1390 
author = {Lawrence C. Paulson}, 

1391 
title = {Natural Deduction as Higherorder Resolution}, 

1392 
journal = JLP, 

1393 
volume = 3, 

1394 
pages = {237258}, 

1395 
year = 1986, 

6619  1396 
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82lcphigherorderresolution.dvi.gz}}} 
6592  1397 

1398 
@Article{paulsonsetI, 

1399 
author = {Lawrence C. Paulson}, 

1400 
title = {Set Theory for Verification: {I}. {From} 

1401 
Foundations to Functions}, 

1402 
journal = JAR, 

1403 
volume = 11, 

1404 
number = 3, 

1405 
pages = {353389}, 

1406 
year = 1993, 

14385  1407 
url = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Sets/setI.pdf}}} 
6592  1408 

1409 
@Article{paulsonsetII, 

1410 
author = {Lawrence C. Paulson}, 

1411 
title = {Set Theory for Verification: {II}. {Induction} and 

1412 
Recursion}, 

1413 
journal = JAR, 

1414 
volume = 15, 

1415 
number = 2, 

1416 
pages = {167215}, 

1417 
year = 1995, 

6619  1418 
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312lcpsetII.ps.gz}}} 
6592  1419 

1420 
@article{paulson85, 

1421 
author = {Lawrence C. Paulson}, 

1422 
title = {Verifying the Unification Algorithm in {LCF}}, 

1423 
journal = SCP, 

1424 
volume = 5, 

1425 
pages = {143170}, 

1426 
year = 1985} 

1427 
