author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 51058  98c48d023136 
child 52078  d9c04fb297e1 
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 

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

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

167 
booktitle = {Handbook of Automated Reasoning}, 

168 
publisher = {Elsevier}, 

169 
year = 2001, 

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

171 
} 

172 

40942  173 
@inproceedings{cvc3, 
174 
author = {Clark Barrett and Cesare Tinelli}, 

175 
title = {{CVC3}}, 

176 
booktitle = {CAV}, 

177 
editor = {Werner Damm and Holger Hermanns}, 

178 
volume = {4590}, 

179 
series = LNCS, 

180 
pages = {298302}, 

181 
publisher = {Springer}, 

182 
year = {2007} 

183 
} 

184 

6592  185 
@incollection{basin91, 
186 
author = {David Basin and Matt Kaufmann}, 

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

188 
Comparison}, 

189 
crossref = {huetplotkin91}, 

190 
pages = {89119}} 

191 

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

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

195 
Markus Wenzel}, 

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

12660  197 
note = {Part of the Isabelle distribution, 
12466  198 
\url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, 
12660  199 
year = 2002 
12466  200 
} 
201 

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

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

205 
{I}sabelle/{I}sar}, 

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

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

9567  209 
series = {LNCS}, 
9599  210 
year = 2000 
9567  211 
} 
6624  212 

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

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

216 
crossref = {tphols2001}} 

217 

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

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

219 
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

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

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

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

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

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

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

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

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

228 

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

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

230 
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

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

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

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

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

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

236 

11619  237 
@INPROCEEDINGS{BerghoferNipkow:2000:TPHOL, 
238 
crossref = "tphols2000", 

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

240 
author = "Stefan Berghofer and Tobias Nipkow", 

241 
pages = "3852"} 

242 

33191  243 
@inproceedings{berghofernipkow2004, 
244 
author = {Stefan Berghofer and Tobias Nipkow}, 

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

246 
pages = {230239}, 

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

248 
booktitle = {{SEFM} 2004}, 

249 
publisher = IEEE, 

250 
year = 2004} 

251 

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

254 
title = {Executing Higher Order Logic}, 

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

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

257 
series = LNCS, 

258 
publisher = Springer, 

13009  259 
volume = 2277, 
12612  260 
year = 2002} 
261 

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

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

266 
crossref = {tphols99}} 

6624  267 

30170  268 

269 
@InProceedings{BezemCoquand:2005, 

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

271 
title = {Automating {Coherent Logic}}, 

272 
booktitle = {LPAR12}, 

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

274 
volume = 3835, 

275 
series = LNCS, 

276 
publisher = Springer} 

277 

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

280 

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

283 
publisher=PH,year=1998} 

284 

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

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

286 
author = {Jasmin Christian Blanchette}, 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

287 
title = {Picking Nits: A User's Guide to {N}itpick for {I}sabelle/{HOL}}, 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

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

289 
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

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

291 

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

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

293 
author = {Jasmin Christian Blanchette}, 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

294 
title = {Hammering Away: A User's Guide to {S}ledgehammer for {I}sabelle/{HOL}}, 
de9d43c427ae
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
blanchet
parents:
40942
diff
changeset

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

296 
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

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

298 

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

33191  301 
author = "Jasmin Christian Blanchette and Tobias Nipkow", 
36926  302 
crossref = {itp2010}} 
303 

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

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

305 
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

306 
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

307 
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

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

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

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

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

312 

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

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

314 
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

315 
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

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

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

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

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

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

321 
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

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

323 
% 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

324 

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

327 
title={Sledgehammer: Judgement Day}, 

328 
booktitle={Automated Reasoning: IJCAR 2010}, 

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

330 
publisher=Springer, 

331 
series=LNCS, 

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

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

333 
pages = "107121", 
36926  334 
year=2010} 
33191  335 

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

338 
Overbeek and Mark Stickel and Lawrence Wos}, 

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

340 
Axioms}, 

341 
journal = JAR, 

342 
year = 1986, 

343 
volume = 2, 

344 
number = 3, 

345 
pages = {287327}} 

346 

347 
@book{bm79, 

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

349 
title = {A Computational Logic}, 

350 
publisher = {Academic Press}, 

351 
year = 1979} 

352 

353 
@book{bm88book, 

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

355 
title = {A Computational Logic Handbook}, 

356 
publisher = {Academic Press}, 

357 
year = 1988} 

358 

44093  359 
@inproceedings{satallax, 
360 
author = "Chad E. Brown", 

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

362 
booktitle = {Automated Deduction  CADE23}, 

363 
publisher = Springer, 

364 
series = LNCS, 

365 
volume = 6803, 

366 
pages = "147161", 

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

368 
year = 2011} 

369 

6592  370 
@Article{debruijn72, 
371 
author = {N. G. de Bruijn}, 

372 
title = {Lambda Calculus Notation with Nameless Dummies, 

373 
a Tool for Automatic Formula Manipulation, 

374 
with Application to the {ChurchRosser Theorem}}, 

375 
journal = {Indag. Math.}, 

376 
volume = 34, 

377 
pages = {381392}, 

378 
year = 1972} 

379 

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

383 
crossref = {tphols2007}, 

384 
pages = {3853} 

385 
} 

23187  386 

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

391 
} 

392 
% pages = {3853} 

393 

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

396 
title = {A Logic of Authentication}, 

397 
journal = PROYAL, 

398 
year = 1989, 

399 
volume = 426, 

400 
pages = {233271}} 

401 

6592  402 
%C 
403 

50130  404 
@PhdThesis{Chaiebthesis, 
405 
author = {Amine Chaieb}, 

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

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

408 
year = 2008, 

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

410 

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

413 
title = {Context aware Calculation and Deduction  

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

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

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

417 
series = LNAI, 

418 
volume = 4573, 

419 
year = 2007, 

420 
publisher = Springer 

421 
} 

422 

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

425 
title = {Reasoning with Inductively Defined Relations in the 

426 
{HOL} Theorem Prover}, 

427 
institution = CUCL, 

428 
year = 1992, 

429 
number = 265, 

430 
month = Aug} 

431 

432 
@Book{charniak80, 

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

434 
title = {Artificial Intelligence Programming}, 

435 
publisher = {Lawrence Erlbaum Associates}, 

436 
year = 1980} 

437 

438 
@article{church40, 

439 
author = "Alonzo Church", 

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

441 
journal = JSL, 

442 
year = 1940, 

443 
volume = 5, 

444 
pages = "5668"} 

445 

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

448 

6592  449 
@PhdThesis{coen92, 
450 
author = {Martin D. Coen}, 

451 
title = {Interactive Program Derivation}, 

452 
school = {University of Cambridge}, 

453 
note = {Computer Laboratory Technical Report 272}, 

454 
month = nov, 

455 
year = 1992} 

456 

457 
@book{constable86, 

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

459 
title = {Implementing Mathematics with the Nuprl Proof 

460 
Development System}, 

461 
publisher = Prentice, 

462 
year = 1986} 

463 

464 
%D 

465 

6745  466 
@Book{daveypriestley, 
6592  467 
author = {B. A. Davey and H. A. Priestley}, 
468 
title = {Introduction to Lattices and Order}, 

469 
publisher = CUP, 

470 
year = 1990} 

471 

472 
@Book{devlin79, 

473 
author = {Keith J. Devlin}, 

474 
title = {Fundamentals of Contemporary Set Theory}, 

475 
publisher = {Springer}, 

476 
year = 1979} 

477 

478 
@book{dummett, 

479 
author = {Michael Dummett}, 

480 
title = {Elements of Intuitionism}, 

481 
year = 1977, 

482 
publisher = {Oxford University Press}} 

483 

40942  484 
@misc{yices, 
485 
author = {Bruno Dutertre and Leonardo de Moura}, 

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

42884  487 
howpublished = "\url{http://yices.csl.sri.com/toolpaper.pdf}", 
40942  488 
year = 2006} 
489 

6592  490 
@incollection{dybjer91, 
491 
author = {Peter Dybjer}, 

10186  492 
title = {Inductive Sets and Families in {MartinL{\"o}f's} Type 
6592  493 
Theory and Their SetTheoretic Semantics}, 
494 
crossref = {huetplotkin91}, 

495 
pages = {280306}} 

496 

497 
@Article{dyckhoff, 

498 
author = {Roy Dyckhoff}, 

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

500 
journal = JSL, 

501 
year = 1992, 

502 
volume = 57, 

503 
number = 3, 

504 
pages = {795807}} 

505 

506 
%F 

507 

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

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

509 
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

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

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

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

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

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

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

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

517 

6592  518 
@InProceedings{felty91a, 
519 
Author = {Amy Felty}, 

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

521 
Deduction Proofs}, 

522 
crossref = {extensions91}, 

523 
pages = {157178}} 

524 

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

527 
title = {Mechanizing Nonstandard Real Analysis}, 

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

529 
year = 2000, 

530 
volume = 3, 

531 
pages = {140190}, 

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

533 
} 

534 

6592  535 
@TechReport{frost93, 
536 
author = {Jacob Frost}, 

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

538 
institution = CUCL, 

539 
number = 308, 

540 
year = 1993, 

541 
month = Aug} 

542 

543 
%revised version of frost93 

544 
@TechReport{frost95, 

545 
author = {Jacob Frost}, 

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

547 
institution = CUCL, 

548 
number = 359, 

549 
year = 1995, 

550 
month = Feb} 

551 

552 
@inproceedings{OBJ, 

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

554 
and J. Meseguer}, 

555 
title = {Principles of {OBJ2}}, 

556 
booktitle = POPL, 

557 
year = 1985, 

558 
pages = {5266}} 

559 

560 
%G 

561 

562 
@book{gallier86, 

563 
author = {J. H. Gallier}, 

564 
title = {Logic for Computer Science: 

565 
Foundations of Automatic Theorem Proving}, 

566 
year = 1986, 

567 
publisher = {Harper \& Row}} 

568 

569 
@Book{galton90, 

570 
author = {Antony Galton}, 

571 
title = {Logic for Information Technology}, 

572 
publisher = {Wiley}, 

573 
year = 1990} 

574 

20506  575 
@Article{Gentzen:1935, 
576 
author = {G. Gentzen}, 

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

578 
journal = {Math. Zeitschrift}, 

579 
year = 1935 

580 
} 

581 

6592  582 
@InProceedings{gimenezcodifying, 
583 
author = {Eduardo Gim{\'e}nez}, 

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

585 
crossref = {types94}, 

586 
pages = {3959} 

587 
} 

588 

9816  589 
@book{girard89, 
590 
author = {JeanYves Girard}, 

591 
title = {Proofs and Types}, 

592 
year = 1989, 

593 
publisher = CUP, 

594 
note = {Translated by Yves LaFont and Paul Taylor}} 

595 

6592  596 
@Book{mgordonhol, 
11205  597 
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

598 
title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic}, 
6592  599 
publisher = CUP, 
600 
year = 1993} 

601 

602 
@book{mgordon79, 

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

604 
Wadsworth}, 

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

606 
year = 1979, 

607 
publisher = {Springer}, 

608 
series = {LNCS 78}} 

609 

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

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

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

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

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

616 

6592  617 
@InProceedings{guntertrees, 
618 
author = {Elsa L. Gunter}, 

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

620 
{HOL}}, 

621 
crossref = {hug93}, 

622 
pages = {141154}} 

623 

624 
%H 

625 

23956  626 
@InProceedings{HaftmannWenzel:2006:classes, 
627 
author = {Florian Haftmann and Makarius Wenzel}, 

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

24628  629 
editor = {T. Altenkirch and C. McBride}, 
630 
booktitle = {Types for Proofs and Programs, TYPES 2006}, 

631 
publisher = {Springer}, 

632 
series = {LNCS}, 

633 
volume = {4502}, 

634 
year = {2007} 

24193  635 
} 
636 

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

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

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

641 
year = 2010, 

38437  642 
publisher = Springer, 
643 
series = LNCS, 

37429  644 
editor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal}, 
38437  645 
volume = 6009 
23956  646 
} 
647 

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

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

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

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

653 
publisher = {Springer}, 

654 
series = {LNCS}, 

32572  655 
volume = {5497}, 
30115  656 
year = {2009} 
657 
} 

658 

45258  659 
@inproceedings{hindleymilner, 
660 
author = {L. Damas and H. Milner}, 

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

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

663 
year = 1982 

664 
} 

665 

22290  666 
@manual{isabelleclasses, 
24193  667 
author = {Florian Haftmann}, 
668 
title = {Haskellstyle type classes with {Isabelle}/{Isar}}, 

669 
institution = TUM, 

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

671 
} 

22290  672 

673 
@manual{isabellecodegen, 

24193  674 
author = {Florian Haftmann}, 
675 
title = {Code generation from Isabelle theories}, 

676 
institution = TUM, 

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

678 
} 

22290  679 

6592  680 
@Book{halmos60, 
681 
author = {Paul R. Halmos}, 

682 
title = {Naive Set Theory}, 

683 
publisher = {Van Nostrand}, 

684 
year = 1960} 

685 

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

688 

6592  689 
@Book{hennessy90, 
690 
author = {Matthew Hennessy}, 

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

692 
Introduction Using Structural Operational Semantics}, 

693 
publisher = {Wiley}, 

694 
year = 1990} 

695 

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

698 
title = "Waldmeister: HighPerformance Equational Deduction", 

699 
journal = JAR, 

700 
volume = 18, 

701 
number = 2, 

702 
pages = {265270}, 

703 
year = 1997} 

704 

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

707 
publisher={AddisonWesley},year=1979} 

708 

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

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

712 
Nonstrict, Purely Functional Language}, 

713 
journal = SIGPLAN, 

714 
year = 1992, 

715 
volume = 27, 

716 
number = 5, 

717 
month = May, 

718 
note = {Version 1.2}} 

719 

720 
@Article{haskelltutorial, 

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

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

723 
journal = SIGPLAN, 

724 
year = 1992, 

725 
volume = 27, 

726 
number = 5, 

727 
month = May} 

728 

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

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

732 
booktitle = {Automated Deduction  CADE23}, 

733 
publisher = Springer, 

734 
series = LNCS, 

44093  735 
volume = 6803, 
736 
pages = "299314", 

42884  737 
editor = "Nikolaj Bj{\o}rner and Viorica SofronieStokkermans", 
44093  738 
year = 2011} 
38602  739 

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

742 

6592  743 
@article{huet75, 
744 
author = {G. P. Huet}, 

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

746 
journal = TCS, 

747 
volume = 1, 

748 
year = 1975, 

749 
pages = {2757}} 

750 

751 
@article{huet78, 

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

753 
title = {Proving and Applying Program Transformations Expressed with 

754 
SecondOrder Patterns}, 

755 
journal = acta, 

756 
volume = 11, 

757 
year = 1978, 

758 
pages = {3155}} 

759 

760 
@inproceedings{huet88, 

10186  761 
author = {G{\'e}rard Huet}, 
6592  762 
title = {Induction Principles Formalized in the {Calculus of 
763 
Constructions}}, 

764 
booktitle = {Programming of Future Generation Computers}, 

765 
editor = {K. Fuchi and M. Nivat}, 

766 
year = 1988, 

767 
pages = {205216}, 

768 
publisher = {Elsevier}} 

769 

10186  770 
@Book{HuthRyanbook, 
771 
author = {Michael Huth and Mark Ryan}, 

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

773 
publisher = CUP, 

774 
year = 2000} 

775 

7041  776 
@InProceedings{Harrison:1996:MizarHOL, 
777 
author = {J. Harrison}, 

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

779 
pages = {203220}, 

780 
crossref = {tphols96}} 

781 

36926  782 
@misc{metis, 
783 
author = "Joe Hurd", 

784 
title = "Metis Theorem Prover", 

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

786 

22290  787 
%J 
788 

789 
@article{haskellrevisedreport, 

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

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

792 
journal = {Journal of Functional Programming}, 

793 
volume = 13, 

794 
number = 1, 

795 
pages = {0255}, 

796 
month = {Jan}, 

797 
year = 2003, 

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

799 

33191  800 
@book{jackson2006, 
801 
author = "Daniel Jackson", 

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

803 
publisher = MIT, 

804 
year = 2006} 

805 

6592  806 
%K 
807 

6670  808 
@InProceedings{kammuellerlocales, 
809 
author = {Florian Kamm{\"u}ller and Markus Wenzel and 

810 
Lawrence C. Paulson}, 

811 
title = {Locales: A Sectioning Concept for {Isabelle}}, 

812 
crossref = {tphols99}} 

813 

8284  814 
@book{Knuth375, 
815 
author={Donald E. Knuth}, 

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

817 
publisher={AddisonWesley}, 

818 
year=1975} 

819 

820 
@Article{korf85, 

821 
author = {R. E. Korf}, 

822 
title = {DepthFirst IterativeDeepening: an Optimal Admissible 

823 
Tree Search}, 

824 
journal = AI, 

825 
year = 1985, 

826 
volume = 27, 

827 
pages = {97109}} 

6607  828 

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

831 
author = "Konstantin Korovin", 

832 
editor = "Renate A. Schmidt", 

833 
booktitle = {Automated Deduction  CADE22}, 

834 
series = "LNAI", 

835 
volume = {5663}, 

836 
pages = "163166", 

837 
year = 2009, 

838 
publisher = "Springer"} 

839 

840 
@inproceedings{korovinsticksel2010, 

841 
author = {Konstantin Korovin and 

842 
Christoph Sticksel}, 

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

844 
pages = {196202}, 

845 
booktitle={Automated Reasoning: IJCAR 2010}, 

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

847 
publisher = Springer, 

848 
series = LNCS, 

849 
volume = 6173, 

850 
year = 2010} 

851 

23187  852 
@InProceedings{krauss2006, 
853 
author = {Alexander Krauss}, 

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

855 
crossref = {ijcar2006}, 

856 
pages = {589603}} 

857 

33856  858 
@PhdThesis{krauss_phd, 
859 
author = {Alexander Krauss}, 

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

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

862 
year = {2009}, 

863 
address = {Germany} 

864 
} 

865 

24524  866 
@manual{isabellefunction, 
867 
author = {Alexander Krauss}, 

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

869 
institution = TUM, 

25280  870 
note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}} 
24524  871 
} 
872 

6592  873 
@Book{kunen80, 
874 
author = {Kenneth Kunen}, 

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

876 
publisher = NH, 

877 
year = 1980} 

878 

11246  879 
%L 
880 

22290  881 
@manual{OCaml, 
882 
author = {Xavier Leroy and others}, 

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

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

885 

38602  886 
@incollection{lochbihler2010, 
887 
title = "Coinduction", 

888 
author = "Andreas Lochbihler", 

889 
booktitle = "The Archive of Formal Proofs", 

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

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

892 
month = "Feb.", 

893 
year = 2010} 

894 

43579  895 
@book{loveland78, 
896 
author = "D. W. Loveland", 

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

898 
year = 1978, 

899 
publisher = "NorthHolland Publishing Co."} 

900 

11246  901 
@InProceedings{lowefdr, 
902 
author = {Gavin Lowe}, 

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

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

905 
booktitle = {Tools and Algorithms for the Construction and Analysis 

906 
of Systems: second international workshop, TACAS '96}, 

907 
editor = {T. Margaria and B. Steffen}, 

908 
series = {LNCS 1055}, 

909 
year = 1996, 

910 
publisher = {Springer}, 

911 
pages = {147166}} 

912 

6592  913 
%M 
914 

915 
@Article{mw81, 

916 
author = {Zohar Manna and Richard Waldinger}, 

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

918 
journal = SCP, 

919 
year = 1981, 

920 
volume = 1, 

921 
number = 1, 

922 
pages = {548}} 

923 

924 
@InProceedings{martinnipkow, 

925 
author = {Ursula Martin and Tobias Nipkow}, 

926 
title = {Ordered Rewriting and Confluence}, 

927 
crossref = {cade10}, 

928 
pages = {366380}} 

929 

930 
@book{martinlof84, 

10186  931 
author = {Per MartinL{\"o}f}, 
6592  932 
title = {Intuitionistic type theory}, 
933 
year = 1984, 

934 
publisher = {Bibliopolis}} 

935 

936 
@incollection{melham89, 

937 
author = {Thomas F. Melham}, 

938 
title = {Automating Recursive Type Definitions in Higher Order 

939 
Logic}, 

940 
pages = {341386}, 

941 
crossref = {birtwistle89}} 

942 

29728  943 
@Article{Miller:1991, 
944 
author = {Dale Miller}, 

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

946 
and Simple Unification}, 

947 
journal = {Journal of Logic and Computation}, 

948 
year = 1991, 

949 
volume = 1, 

950 
number = 4 

951 
} 

952 

6592  953 
@Article{millermixed, 
954 
Author = {Dale Miller}, 

955 
Title = {Unification Under a Mixed Prefix}, 

956 
journal = JSC, 

957 
volume = 14, 

958 
number = 4, 

959 
pages = {321358}, 

960 
Year = 1992} 

961 

962 
@Article{milner78, 

963 
author = {Robin Milner}, 

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

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

966 
year = 1978, 

967 
volume = 17, 

968 
pages = {348375}} 

969 

970 
@TechReport{milnerind, 

971 
author = {Robin Milner}, 

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

973 
institution = Edinburgh, 

974 
year = 1980, 

975 
type = {note}} 

976 

977 
@Article{milnercoind, 

978 
author = {Robin Milner and Mads Tofte}, 

979 
title = {Coinduction in Relational Semantics}, 

980 
journal = TCS, 

981 
year = 1991, 

982 
volume = 87, 

983 
pages = {209220}} 

984 

985 
@Book{milner89, 

986 
author = {Robin Milner}, 

987 
title = {Communication and Concurrency}, 

988 
publisher = Prentice, 

989 
year = 1989} 

990 

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

993 

6592  994 
@PhdThesis{monahan84, 
995 
author = {Brian Q. Monahan}, 

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

997 
school = {University of Edinburgh}, 

998 
year = 1984} 

999 

6607  1000 
@article{MuellerNvOS99, 
1001 
author= 

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

9599  1005 
@Manual{Muzalewski:Mizar, 
1006 
title = {An Outline of {PC} {Mizar}}, 

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

1008 
organization = {Fondation of Logic, Mathematics and Informatics 

1009 
 Mizar Users Group}, 

1010 
year = 1993, 

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

1012 
} 

1013 

6592  1014 
%N 
1015 

1016 
@InProceedings{NaraschewskiWTPHOLs98, 

1017 
author = {Wolfgang Naraschewski and Markus Wenzel}, 

1018 
title = 

7041  1019 
{ObjectOriented Verification based on Record Subtyping in 
1020 
HigherOrder Logic}, 

1021 
crossref = {tphols98}} 

6592  1022 

1023 
@inproceedings{nazarethnipkow, 

1024 
author = {Dieter Nazareth and Tobias Nipkow}, 

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

1026 
crossref = {tphols96}, 

1027 
pages = {331345}, 

1028 
year = 1996} 

1029 

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

1032 
title = "Using Encryption for Authentication in Large Networks 

1033 
of Computers", 

1034 
journal = cacm, 

1035 
volume = 21, 

1036 
number = 12, 

1037 
pages = "993999", 

1038 
month = dec, 

1039 
year = 1978} 

1040 

6592  1041 
@inproceedings{nipkowW, 
1042 
author = {Wolfgang Naraschewski and Tobias Nipkow}, 

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

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

10186  1045 
editor = {E. Gim{\'e}nez and C. PaulinMohring}, 
6592  1046 
publisher = Springer, 
1047 
series = LNCS, 

1048 
volume = 1512, 

1049 
pages = {317332}, 

1050 
year = 1998} 

1051 

8892  1052 
@InCollection{nipkowsorts93, 
1053 
author = {T. Nipkow}, 

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

1055 
booktitle = {Logical Environments}, 

1056 
publisher = CUP, 

1057 
year = 1993, 

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

1059 
pages = {164188} 

1060 
} 

1061 

1062 
@Misc{nipkowtypes93, 

1063 
author = {Tobias Nipkow}, 

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

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

1066 
year = 1993 

1067 
} 

1068 

6592  1069 
@inproceedings{NipkowCR, 
1070 
author = {Tobias Nipkow}, 

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

1072 
booktitle = {Automated Deduction  CADE13}, 

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

1074 
publisher = Springer, 

1075 
series = LNCS, 

1076 
volume = 1104, 

1077 
pages = {733747}, 

1078 
year = 1996} 

1079 

1080 
% WAS NipkowLICS93 

1081 
@InProceedings{nipkowpatterns, 

1082 
title = {Functional Unification of HigherOrder Patterns}, 

1083 
author = {Tobias Nipkow}, 

1084 
pages = {6474}, 

1085 
crossref = {lics8}, 

6745  1086 
url = {\url{ftp://ftp.informatik.tumuenchen.de/local/lehrstuhl/nipkow/lics93.html}}, 
6592  1087 
keywords = {unification}} 
1088 

1089 
@article{nipkowIMP, 

1090 
author = {Tobias Nipkow}, 

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

1092 
journal = FAC, 

1093 
volume = 10, 

1094 
pages = {171186}, 

1095 
year = 1998} 

1096 

15429  1097 
@inproceedings{NipkowTYPES02, 
1098 
author = {Tobias Nipkow}, 

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

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

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

1102 
year = 2003, 

1103 
publisher = Springer, 

1104 
series = LNCS, 

1105 
volume = 2646, 

1106 
pages = {259278}} 

1107 

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

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

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

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

6592  1115 
@article{nipkowprehofer, 
1116 
author = {Tobias Nipkow and Christian Prehofer}, 

1117 
title = {Type Reconstruction for Type Classes}, 

1118 
journal = JFP, 

1119 
volume = 5, 

1120 
number = 2, 

1121 
year = 1995, 

1122 
pages = {201224}} 

1123 

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

1126 
title = {Type checking type classes}, 

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

1128 
year = 1993 

1129 
} 

1130 

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

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

14147  1135 
year = 2002, 
33191  1136 
series = LNCS, 
1137 
volume = 2283} 

14147  1138 

6592  1139 
@Article{noel, 
1140 
author = {Philippe No{\"e}l}, 

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

1142 
journal = JAR, 

1143 
volume = 10, 

1144 
number = 1, 

1145 
pages = {1558}, 

1146 
year = 1993} 

1147 

1148 
@book{nordstrom90, 

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

6592  1151 
Introduction}, 
1152 
publisher = {Oxford University Press}, 

1153 
year = 1990} 

1154 

1155 
%O 

1156 

38814  1157 
@TechReport{scalaoverviewtechreport, 
1158 
author = {Martin Odersky and al.}, 

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

1160 
institution = {EPFL Lausanne, Switzerland}, 

1161 
year = 2004, 

1162 
number = {IC/2004/64} 

1163 
} 

1164 

46286  1165 
@Article{Oppen:1980, 
1166 
author = {D. C. Oppen}, 

1167 
title = {Pretty Printing}, 

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

1169 
year = 1980, 

1170 
volume = 2, 

1171 
number = 4} 

1172 

6592  1173 
@Manual{pvslanguage, 
1174 
title = {The {PVS} specification language}, 

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

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

1177 
address = {Menlo Park, CA}, 

6745  1178 
note = {Beta release}, 
6592  1179 
year = 1993, 
1180 
month = apr, 

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

1183 
%P 

1184 

1185 
% replaces paulin92 

1186 
@InProceedings{paulintlca, 

1187 
author = {Christine PaulinMohring}, 

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

1189 
Properties}, 

1190 
crossref = {tlca93}, 

1191 
pages = {328345}} 

1192 

50122  1193 
@Article{paulson:1983, 
1194 
author = {L. C. Paulson}, 

1195 
title = {A higherorder implementation of rewriting}, 

1196 
journal = {Science of Computer Programming}, 

1197 
year = 1983, 

1198 
volume = 3, 

1199 
pages = {119149}, 

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

1201 

6592  1202 
@InProceedings{paulsonCADE, 
1203 
author = {Lawrence C. Paulson}, 

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

1205 
Definitions}, 

1206 
pages = {148161}, 

1207 
crossref = {cade12}} 

1208 

1209 
@InProceedings{paulsonCOLOG, 

1210 
author = {Lawrence C. Paulson}, 

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

1212 
{Isabelle})}, 

1213 
pages = {246274}, 

1214 
crossref = {colog88}, 

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

1217 
@Article{paulsoncoind, 

1218 
author = {Lawrence C. Paulson}, 

1219 
title = {Mechanizing Coinduction and Corecursion in HigherOrder 

1220 
Logic}, 

1221 
journal = JLC, 

1222 
year = 1997, 

1223 
volume = 7, 

1224 
number = 2, 

1225 
month = mar, 

1226 
pages = {175204}} 

1227 

12616  1228 
@manual{isabelleintro, 
1229 
author = {Lawrence C. Paulson}, 

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

1233 

1234 
@manual{isabellelogics, 

1235 
author = {Lawrence C. Paulson}, 

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

1237 
institution = CUCL, 

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

1239 

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

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

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

6607  1245 

1246 
@manual{isabelleZF, 

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

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

6592  1251 

1252 
@article{paulsonfound, 

1253 
author = {Lawrence C. Paulson}, 

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

1255 
journal = JAR, 

1256 
volume = 5, 

1257 
number = 3, 

1258 
pages = {363397}, 

1259 
year = 1989, 

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

1262 
%replaces paulsonfinal 

1263 
@Article{paulsonmscs, 

1264 
author = {Lawrence C. Paulson}, 

7991  1265 
title = {Final Coalgebras as Greatest Fixed Points 
1266 
in {ZF} Set Theory}, 

6592  1267 
journal = {Mathematical Structures in Computer Science}, 
1268 
year = 1999, 

1269 
volume = 9, 

23505  1270 
number = 5, 
1271 
pages = {545567}} 

6592  1272 

1273 
@InCollection{paulsongeneric, 

1274 
author = {Lawrence C. Paulson}, 

1275 
title = {Generic Automatic Proof Tools}, 

1276 
crossref = {wosfest}, 

1277 
chapter = 3} 

1278 

1279 
@Article{paulsongr, 

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

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

1282 
Choice}, 

1283 
journal = JAR, 

1284 
year = 1996, 

1285 
volume = 17, 

1286 
number = 3, 

1287 
month = dec, 

1288 
pages = {291323}} 

1289 

14210  1290 
@InCollection{paulsonfixedptmilner, 
1291 
author = {Lawrence C. Paulson}, 

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

1293 
(Co)datatype Definitions}, 

1294 
pages = {187211}, 

1295 
crossref = {milnerfest}} 

1296 

1297 
@book{milnerfest, 

1298 
title = {Proof, Language, and Interaction: 

1299 
Essays in Honor of {Robin Milner}}, 

1300 
booktitle = {Proof, Language, and Interaction: 

1301 
Essays in Honor of {Robin Milner}}, 

33191  1302 
publisher = MIT, 
14210  1303 
year = 2000, 
1304 
editor = {Gordon Plotkin and Colin Stirling and Mads Tofte}} 

1305 

6592  1306 
@InCollection{paulsonhandbook, 
1307 
author = {Lawrence C. Paulson}, 

1308 
title = {Designing a Theorem Prover}, 

1309 
crossref = {handbklics2}, 

1310 
pages = {415475}} 

1311 

1312 
@Book{paulsonisabook, 

1313 
author = {Lawrence C. Paulson}, 

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

1315 
publisher = {Springer}, 

1316 
year = 1994, 

1317 
note = {LNCS 828}} 

1318 

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

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

1322 
publisher = {Springer}, 

1323 
year = 2002, 

1324 
note = {LNCS 2283}} 

1325 

6592  1326 
@InCollection{paulsonmarkt, 
1327 
author = {Lawrence C. Paulson}, 

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

1329 
booktitle = {Mathematical Methods in Program Development: 

1330 
Summer School Marktoberdorf 1996}, 

1331 
publisher = {Springer}, 

1332 
pages = {461498}, 

1333 
year = {Published 1997}, 

1334 
editor = {Manfred Broy}, 

1335 
series = {NATO ASI Series F}} 

1336 

1337 
%replaces PaulsonML and paulson91 

1338 
@book{paulsonml2, 

1339 
author = {Lawrence C. Paulson}, 

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

1341 
year = 1996, 

1342 
edition = {2nd}, 

1343 
publisher = CUP} 

1344 

1345 
@article{paulsonnatural, 

1346 
author = {Lawrence C. Paulson}, 

1347 
title = {Natural Deduction as Higherorder Resolution}, 

1348 
journal = JLP, 

1349 
volume = 3, 

1350 
pages = {237258}, 

1351 
year = 1986, 

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

1354 
@Article{paulsonsetI, 

1355 
author = {Lawrence C. Paulson}, 

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

1357 
Foundations to Functions}, 

1358 
journal = JAR, 

1359 
volume = 11, 

1360 
number = 3, 

1361 
pages = {353389}, 

1362 
year = 1993, 

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

1365 
@Article{paulsonsetII, 

1366 
author = {Lawrence C. Paulson}, 

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

1368 
Recursion}, 

1369 
journal = JAR, 

1370 
volume = 15, 

1371 
number = 2, 

1372 
pages = {167215}, 

1373 
year = 1995, 

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

1376 
@article{paulson85, 

1377 
author = {Lawrence C. Paulson}, 

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

1379 
journal = SCP, 

1380 
volume = 5, 

1381 
pages = {143170}, 

1382 
year = 1985} 

1383 

11564  1384 
%replaces PaulsonLCF 
6592  1385 
@book{paulson87, 
1386 
author = {Lawrence C. Paulson}, 

1387 
title = {Logic and Computation: Interactive proof with Cambridge 

1388 
LCF}, 

1389 
year = 1987, 

1390 
publisher = CUP} 

1391 

1392 
@incollection{paulson700, 

1393 
author = {Lawrence C. Paulson}, 

1394 
title = {{Isabelle}: The Next 700 Theorem Provers}, 

1395 
crossref = {odifreddi90}, 

1396 
pages = {361386}, 

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

1399 
% replaces paulsonns and paulsonsecurity 

1400 
@Article{paulsonjcs, 

1401 
author = {Lawrence C. Paulson}, 

1402 
title = {The Inductive Approach to Verifying Cryptographic Protocols}, 

1403 
journal = JCS, 

1404 
year = 1998, 

1405 
volume = 6, 

1406 
pages = {85128}} 

1407 

11246  1408 
@Article{paulsontls, 
1409 
author = {Lawrence C. Paulson}, 

1410 
title = {Inductive Analysis of the {Internet} Protocol {TLS}}, 

1411 
journal = TISSEC, 

1412 
month = aug, 

1413 
year = 1999, 

1414 
volume = 2, 

1415 
number = 3, 

1416 
pages = {332351}} 

21074  1417 

1418 
@Article{paulsonyahalom, 

1419 
author = {Lawrence C. Paulson}, 

1420 
title = {Relations Between Secrets: 

1421 
Two Formal Analyses of the {Yahalom} Protocol}, 

1422 
journal = JCS, 

23505  1423 
volume = 9, 
1424 
number = 3, 

1425 
pages = {197216}, 

1426 
year = 2001}} 

11246  1427 

6592  1428 
@article{pelletier86, 
1429 
author = {F. J. Pelletier}, 

1430 
title = {Seventyfive Problems for Testing Automatic Theorem 