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;
oheimb@11565
     1
@misc{NanoJava,
oheimb@11565
     2
        author={Oheimb, David von and Tobias Nipkow},
oheimb@11565
     3
        title={Hoare Logic for {NanoJava}: Auxiliary Variables,
oheimb@11565
     4
    Side Effects and Virtual Methods revisited},
oheimb@11565
     5
        year = {2002},
oheimb@11565
     6
        abstract = {We give a Hoare logic for NanoJava, 
oheimb@11565
     7
  a small fragment of Java with essentially just classes.  
oheimb@11565
     8
  The logic is proved sound and (relatively) complete within Isabelle/HOL.  
oheimb@11565
     9
  We introduce an elegant new approach for expressing auxiliary variables: 
oheimb@11565
    10
  by universal quantification on the outer logical level. 
oheimb@11565
    11
  Furthermore, we give simple means of handling side-effecting expressions 
oheimb@11565
    12
  and dynamic binding within method calls.},
oheimb@11565
    13
        CRClassification = {D.3.1, F.3.2},
oheimb@11565
    14
        CRGenTerms = {Languages, Reliability, Theory, Verification},
oheimb@11565
    15
        url = {\url{http://isabelle.in.tum.de/Bali/papers/NanoJava.html}},
oheimb@11565
    16
        note = {Submitted for publication.}
oheimb@11565
    17
}
oheimb@11565
    18
oheimb@11376
    19
@inproceedings{NipkowOP00,
oheimb@11376
    20
        author={Tobias Nipkow and Oheimb, David von and Cornelia Pusch},
oheimb@11376
    21
        title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},
oheimb@11376
    22
        booktitle = {Foundations of Secure Computation},
oheimb@11376
    23
        series= {NATO Science Series F: Computer and Systems Sciences},
oheimb@11376
    24
        volume = {175},
oheimb@11376
    25
        year = {2000},
oheimb@11376
    26
        publisher = {IOS Press},
oheimb@11376
    27
        editor = {Friedrich L. Bauer and Ralf Steinbr{\"u}ggen},
oheimb@11376
    28
        abstract = {This paper introduces the subset $micro$Java of Java,
oheimb@11376
    29
essentially by omitting everything but classes.
oheimb@11376
    30
The type system and semantics of this language
oheimb@11376
    31
(and a corresponding abstract Machine $micro$JVM)
oheimb@11376
    32
are formalized in the theorem prover Isabelle/HOL.
oheimb@11376
    33
Type safety both of $micro$Java and the $micro$JVM
oheimb@11376
    34
are mechanically verified.
oheimb@11376
    35
oheimb@11376
    36
To make the paper self-contained, it starts with
oheimb@11376
    37
introductions to Isabelle/HOL and the art of
oheimb@11376
    38
embedding languages in theorem provers.},
oheimb@11376
    39
        CRClassification = {D.3.1, F.3.2},
oheimb@11376
    40
        CRGenTerms = {Languages, Reliability, Theory, Verification},
oheimb@11376
    41
        url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},
oheimb@11376
    42
        pages = {117--144}
oheimb@11376
    43
}
oheimb@11376
    44
oheimb@11376
    45
oheimb@11376
    46
@article{DvO-CPE01,
oheimb@11376
    47
        author = {David von Oheimb},
oheimb@11376
    48
        title = {Hoare Logic for {J}ava in {Isabelle/HOL}},
oheimb@11376
    49
        journal = {Concurrency: Practice and Experience},
oheimb@11376
    50
        year = {2001},
oheimb@11507
    51
        volume = 598,
oheimb@11507
    52
        pages = {??--??+43},
oheimb@11376
    53
        url = {http://www4.in.tum.de/papers/DvO-CPE01.html},
oheimb@11376
    54
        abstract = {
oheimb@11376
    55
This article presents a Hoare-style calculus for a substantial subset 
oheimb@11376
    56
of Java Card, which we call Java_light. In particular, the language 
oheimb@11376
    57
includes side-effecting expressions, mutual recursion, dynamic method 
oheimb@11376
    58
binding, full exception handling, and static class initialization.
oheimb@11376
    59
oheimb@11376
    60
The Hoare logic of partial correctness is proved not only sound (w.r.t.
oheimb@11376
    61
our operational semantics of Java_light, described in detail elsewhere)
oheimb@11376
    62
but even complete. It is the first logic for an object-oriented 
oheimb@11376
    63
language that is provably complete.
oheimb@11376
    64
The completeness proof uses a refinement of the Most General Formula 
oheimb@11376
    65
approach. The proof of soundness gives new insights into the role of 
oheimb@11376
    66
type safety. Further by-products of this work are a new general 
oheimb@11376
    67
methodology for handling side-effecting expressions and their results, 
oheimb@11376
    68
the discovery of the strongest possible rule of consequence, and a 
oheimb@11376
    69
flexible Call rule for mutual recursion. 
oheimb@11376
    70
We also give a small but non-trivial application example.
oheimb@11376
    71
oheimb@11376
    72
All definitions and proofs have been done formally with the interactive 
oheimb@11376
    73
theorem prover Isabelle/HOL. This guarantees not only rigorous definitions, 
oheimb@11376
    74
but also gives maximal confidence in the results obtained.},
oheimb@11376
    75
        CRClassification = {D.2.4, D.3.1, F.3.1},
oheimb@11376
    76
        CRGenTerms = {Languages, Verification, Theory},
oheimb@11376
    77
        note = {\url{http://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear}
oheimb@11376
    78
}