| 
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  | 
@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
 | 
| 
 | 
    17  | 
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
  | 
| 
 | 
    18  | 
publisher=Springer,series=LNCS,volume=2283,year=2002,
  | 
| 
 | 
    19  | 
note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
 | 
| 
 | 
    20  | 
  | 
| 
25427
 | 
    21  | 
@article{KleinN-TOPLAS,author={Gerwin Klein and Tobias Nipkow},
 | 
| 
 | 
    22  | 
title={A Machine-Checked Model for a {Java}-Like Language, Virtual Machine and Compiler},
 | 
| 
 | 
    23  | 
journal=TOPLAS,volume = {28}, number = {4}, year = {2006}, pages = {619--695},
 | 
| 
 | 
    24  | 
doi = {http://doi.acm.org/10.1145/1146809.1146811}}
 | 
| 
13999
 | 
    25  | 
  | 
| 
 | 
    26  | 
@InProceedings{Rudnicki92,author={P. Rudnicki},
 | 
| 
 | 
    27  | 
title={An Overview of the {Mizar} Project},
 | 
| 
 | 
    28  | 
booktitle={Workshop on Types for Proofs and Programs},
 | 
| 
 | 
    29  | 
year=1992,organization={Chalmers University of Technology}}
 | 
| 
 | 
    30  | 
  | 
| 
 | 
    31  | 
@manual{Isar-Ref-Man,author="Markus Wenzel",
 | 
| 
 | 
    32  | 
title="The Isabelle/Isar Reference Manual",
  | 
| 
 | 
    33  | 
organization={Technische Universit{\"a}t M{\"u}nchen},year=2002,
 | 
| 
 | 
    34  | 
note={\url{http://isabelle.in.tum.de/dist/Isabelle2002/doc/isar-ref.pdf}}}
 | 
| 
 | 
    35  | 
  | 
| 
 | 
    36  | 
@article{WenzelW-JAR,author={Markus Wenzel and Freek Wiedijk},
 | 
| 
 | 
    37  | 
title={A comparison of the mathematical proof languages {Mizar} and {Isar}},
 | 
| 
25403
 | 
    38  | 
journal=JAR,year=2002,pages={389--411}}
 | 
| 
13999
 | 
    39  | 
  |