doc-src/TutorialI/IsarOverview/Isar/document/root.bib
author nipkow
Wed, 02 Oct 2002 17:03:51 +0200
changeset 13621 75ae05e894fa
parent 13620 61a23a43b783
child 13768 1764a81b7a0a
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13294
5e2016d151bd *** empty log message ***
nipkow
parents: 13267
diff changeset
     1
@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
5e2016d151bd *** empty log message ***
nipkow
parents: 13267
diff changeset
     2
@string{Springer="Springer-Verlag"}
5e2016d151bd *** empty log message ***
nipkow
parents: 13267
diff changeset
     3
13619
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
     4
@InProceedings{BauerW-TPHOLs01,
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
     5
author={Gertrud Bauer and Markus Wenzel},
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
     6
title={Calculational Reasoning Revisited --- an {Isabelle/Isar} Experience},
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
     7
booktitle={Theorem Proving in Higher Order Logics, TPHOLs 2001},
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
     8
editor={R. Boulton and P. Jackson},
13620
61a23a43b783 *** empty log message ***
nipkow
parents: 13619
diff changeset
     9
year=2001,publisher=Springer,series=LNCS,volume=2152,pages="75--90"}
13619
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    10
13613
531f1f524848 *** empty log message ***
nipkow
parents: 13310
diff changeset
    11
@book{LCF,author="M.C.J. Gordon and Robin Milner and C.P. Wadsworth",
531f1f524848 *** empty log message ***
nipkow
parents: 13310
diff changeset
    12
title="Edinburgh {LCF}: a Mechanised Logic of Computation",
531f1f524848 *** empty log message ***
nipkow
parents: 13310
diff changeset
    13
publisher=Springer,series=LNCS,volume=78,year=1979}
531f1f524848 *** empty log message ***
nipkow
parents: 13310
diff changeset
    14
13619
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    15
@InProceedings{KWP-TPHOLs99,
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    16
author={Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson},
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    17
title={Locales: A Sectioning Concept for {Isabelle}},
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    18
booktitle={Theorem Proving in Higher Order Logics, TPHOLs'99},
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    19
editor={Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Thery},
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    20
year=1999,publisher=Springer,series=LNCS,volume=1690,pages="149--165"}
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    21
13294
5e2016d151bd *** empty log message ***
nipkow
parents: 13267
diff changeset
    22
@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
5e2016d151bd *** empty log message ***
nipkow
parents: 13267
diff changeset
    23
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
13307
cf076cdcfbf3 *** empty log message ***
nipkow
parents: 13294
diff changeset
    24
publisher=Springer,series=LNCS,volume=2283,year=2002,
13310
d694e65127ba *** empty log message ***
nipkow
parents: 13307
diff changeset
    25
note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
13307
cf076cdcfbf3 *** empty log message ***
nipkow
parents: 13294
diff changeset
    26
13620
61a23a43b783 *** empty log message ***
nipkow
parents: 13619
diff changeset
    27
@article{KleinN-TCS,author={Gerwin Klein and Tobias Nipkow},
61a23a43b783 *** empty log message ***
nipkow
parents: 13619
diff changeset
    28
title={Verified Bytecode Verifiers},
13621
75ae05e894fa *** empty log message ***
nipkow
parents: 13620
diff changeset
    29
journal=TCS,year=2002,note={To appear.
75ae05e894fa *** empty log message ***
nipkow
parents: 13620
diff changeset
    30
\url{http://www.in.tum.de/~nipkow/pubs/tcs03.html}}}
13620
61a23a43b783 *** empty log message ***
nipkow
parents: 13619
diff changeset
    31
61a23a43b783 *** empty log message ***
nipkow
parents: 13619
diff changeset
    32
@InProceedings{Rudnicki92,author={P. Rudnicki},
61a23a43b783 *** empty log message ***
nipkow
parents: 13619
diff changeset
    33
title={An Overview of the {Mizar} Project},
61a23a43b783 *** empty log message ***
nipkow
parents: 13619
diff changeset
    34
booktitle={Workshop on Types for Proofs and Programs},
61a23a43b783 *** empty log message ***
nipkow
parents: 13619
diff changeset
    35
year=1992,organization={Chalmers University of Technology}}
61a23a43b783 *** empty log message ***
nipkow
parents: 13619
diff changeset
    36
13307
cf076cdcfbf3 *** empty log message ***
nipkow
parents: 13294
diff changeset
    37
@manual{Isar-Ref-Man,author="Markus Wenzel",
cf076cdcfbf3 *** empty log message ***
nipkow
parents: 13294
diff changeset
    38
title="The Isabelle/Isar Reference Manual",
13310
d694e65127ba *** empty log message ***
nipkow
parents: 13307
diff changeset
    39
organization={Technische Universit{\"a}t M{\"u}nchen},year=2002,
d694e65127ba *** empty log message ***
nipkow
parents: 13307
diff changeset
    40
note={\url{http://isabelle.in.tum.de/dist/Isabelle2002/doc/isar-ref.pdf}}}
13294
5e2016d151bd *** empty log message ***
nipkow
parents: 13267
diff changeset
    41
13267
502f69ea6627 *** empty log message ***
nipkow
parents:
diff changeset
    42
@phdthesis{Wenzel-PhD,author={Markus Wenzel},title={Isabelle/Isar --- A
502f69ea6627 *** empty log message ***
nipkow
parents:
diff changeset
    43
Versatile Environment for Human-Readable Formal Proof Documents},
502f69ea6627 *** empty log message ***
nipkow
parents:
diff changeset
    44
school={Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
13310
d694e65127ba *** empty log message ***
nipkow
parents: 13307
diff changeset
    45
year=2002,
d694e65127ba *** empty log message ***
nipkow
parents: 13307
diff changeset
    46
note={\url{http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html}}}
13619
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    47
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    48
@unpublished{WenzelW-JAR,author={Markus Wenzel and Freek Wiedijk},
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    49
title={A comparison of the mathematical proof languages {Mizar} and {Isar}},
584291949c23 *** empty log message ***
nipkow
parents: 13613
diff changeset
    50
note={Submitted for publication},year=2002}