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 }