13999
|
1 |
@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
|
|
2 |
@string{Springer="Springer-Verlag"}
|
|
3 |
@string{JAR="J. Automated Reasoning"}
|
|
4 |
|
|
5 |
@InProceedings{BauerW-TPHOLs01,
|
|
6 |
author={Gertrud Bauer and Markus Wenzel},
|
|
7 |
title={Calculational Reasoning Revisited --- an {Isabelle/Isar} Experience},
|
|
8 |
booktitle={Theorem Proving in Higher Order Logics, TPHOLs 2001},
|
|
9 |
editor={R. Boulton and P. Jackson},
|
|
10 |
year=2001,publisher=Springer,series=LNCS,volume=2152,pages="75--90"}
|
|
11 |
|
|
12 |
@book{LCF,author="M.C.J. Gordon and Robin Milner and C.P. Wadsworth",
|
|
13 |
title="Edinburgh {LCF}: a Mechanised Logic of Computation",
|
|
14 |
publisher=Springer,series=LNCS,volume=78,year=1979}
|
|
15 |
|
|
16 |
@InProceedings{KWP-TPHOLs99,
|
|
17 |
author={Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson},
|
|
18 |
title={Locales: A Sectioning Concept for {Isabelle}},
|
|
19 |
booktitle={Theorem Proving in Higher Order Logics, TPHOLs'99},
|
|
20 |
editor={Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Thery},
|
|
21 |
year=1999,publisher=Springer,series=LNCS,volume=1690,pages="149--165"}
|
|
22 |
|
|
23 |
@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
|
|
24 |
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
|
|
25 |
publisher=Springer,series=LNCS,volume=2283,year=2002,
|
|
26 |
note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
|
|
27 |
|
|
28 |
@article{KleinN-TCS,author={Gerwin Klein and Tobias Nipkow},
|
|
29 |
title={Verified Bytecode Verifiers},
|
|
30 |
journal=TCS,year=2002,note={To appear.
|
|
31 |
\url{http://www.in.tum.de/~nipkow/pubs/tcs03.html}}}
|
|
32 |
|
|
33 |
@InProceedings{Rudnicki92,author={P. Rudnicki},
|
|
34 |
title={An Overview of the {Mizar} Project},
|
|
35 |
booktitle={Workshop on Types for Proofs and Programs},
|
|
36 |
year=1992,organization={Chalmers University of Technology}}
|
|
37 |
|
|
38 |
@manual{Isar-Ref-Man,author="Markus Wenzel",
|
|
39 |
title="The Isabelle/Isar Reference Manual",
|
|
40 |
organization={Technische Universit{\"a}t M{\"u}nchen},year=2002,
|
|
41 |
note={\url{http://isabelle.in.tum.de/dist/Isabelle2002/doc/isar-ref.pdf}}}
|
|
42 |
|
|
43 |
@phdthesis{Wenzel-PhD,author={Markus Wenzel},title={Isabelle/Isar --- A
|
|
44 |
Versatile Environment for Human-Readable Formal Proof Documents},
|
|
45 |
school={Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
|
|
46 |
year=2002,
|
|
47 |
note={\url{http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html}}}
|
|
48 |
|
|
49 |
@article{WenzelW-JAR,author={Markus Wenzel and Freek Wiedijk},
|
|
50 |
title={A comparison of the mathematical proof languages {Mizar} and {Isar}},
|
|
51 |
journal=JAR,year=2003,note={To appear}}
|
|
52 |
|