src/HOL/NanoJava/document/root.bib
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 11565 ab004c0ecc63 child 68649 f849fc1cb65e permissions -rw-r--r--
tuned proofs;
     1 @misc{NanoJava,

     2         author={Oheimb, David von and Tobias Nipkow},

     3         title={Hoare Logic for {NanoJava}: Auxiliary Variables,

     4     Side Effects and Virtual Methods revisited},

     5         year = {2002},

     6         abstract = {We give a Hoare logic for NanoJava,

     7   a small fragment of Java with essentially just classes.

     8   The logic is proved sound and (relatively) complete within Isabelle/HOL.

     9   We introduce an elegant new approach for expressing auxiliary variables:

    10   by universal quantification on the outer logical level.

    11   Furthermore, we give simple means of handling side-effecting expressions

    12   and dynamic binding within method calls.},

    13         CRClassification = {D.3.1, F.3.2},

    14         CRGenTerms = {Languages, Reliability, Theory, Verification},

    15         url = {\url{http://isabelle.in.tum.de/Bali/papers/NanoJava.html}},

    16         note = {Submitted for publication.}

    17 }

    18

    19 @inproceedings{NipkowOP00,

    20         author={Tobias Nipkow and Oheimb, David von and Cornelia Pusch},

    21         title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},

    22         booktitle = {Foundations of Secure Computation},

    23         series= {NATO Science Series F: Computer and Systems Sciences},

    24         volume = {175},

    25         year = {2000},

    26         publisher = {IOS Press},

    27         editor = {Friedrich L. Bauer and Ralf Steinbr{\"u}ggen},

    28         abstract = {This paper introduces the subset $micro$Java of Java,

    29 essentially by omitting everything but classes.

    30 The type system and semantics of this language

    31 (and a corresponding abstract Machine $micro$JVM)

    32 are formalized in the theorem prover Isabelle/HOL.

    33 Type safety both of $micro$Java and the $micro$JVM

    34 are mechanically verified.

    35

    36 To make the paper self-contained, it starts with

    37 introductions to Isabelle/HOL and the art of

    38 embedding languages in theorem provers.},

    39         CRClassification = {D.3.1, F.3.2},

    40         CRGenTerms = {Languages, Reliability, Theory, Verification},

    41         url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},

    42         pages = {117--144}

    43 }

    44

    45

    46 @article{DvO-CPE01,

    47         author = {David von Oheimb},

    48         title = {Hoare Logic for {J}ava in {Isabelle/HOL}},

    49         journal = {Concurrency: Practice and Experience},

    50         year = {2001},

    51         volume = 598,

    52         pages = {??--??+43},

    53         url = {http://www4.in.tum.de/papers/DvO-CPE01.html},

    54         abstract = {

    55 This article presents a Hoare-style calculus for a substantial subset

    56 of Java Card, which we call Java_light. In particular, the language

    57 includes side-effecting expressions, mutual recursion, dynamic method

    58 binding, full exception handling, and static class initialization.

    59

    60 The Hoare logic of partial correctness is proved not only sound (w.r.t.

    61 our operational semantics of Java_light, described in detail elsewhere)

    62 but even complete. It is the first logic for an object-oriented

    63 language that is provably complete.

    64 The completeness proof uses a refinement of the Most General Formula

    65 approach. The proof of soundness gives new insights into the role of

    66 type safety. Further by-products of this work are a new general

    67 methodology for handling side-effecting expressions and their results,

    68 the discovery of the strongest possible rule of consequence, and a

    69 flexible Call rule for mutual recursion.

    70 We also give a small but non-trivial application example.

    71

    72 All definitions and proofs have been done formally with the interactive

    73 theorem prover Isabelle/HOL. This guarantees not only rigorous definitions,

    74 but also gives maximal confidence in the results obtained.},

    75         CRClassification = {D.2.4, D.3.1, F.3.1},

    76         CRGenTerms = {Languages, Verification, Theory},

    77         note = {\url{http://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear}

    78 }