src/HOL/MicroJava/document/root.bib
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 13067 a59af3a83c61
child 68649 f849fc1cb65e
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 @inproceedings{NipkowOP00,
     2         author={Tobias Nipkow and Oheimb, David von and Cornelia Pusch},
     3         title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},
     4         booktitle = {Foundations of Secure Computation},
     5         series= {NATO Science Series F: Computer and Systems Sciences},
     6         volume = {175},
     7         year = {2000},
     8         publisher = {IOS Press},
     9         editor = {Friedrich L. Bauer and Ralf Steinbr{\"u}ggen},
    10         abstract = {This paper introduces the subset $micro$Java of Java,
    11 essentially by omitting everything but classes.
    12 The type system and semantics of this language
    13 (and a corresponding abstract Machine $micro$JVM)
    14 are formalized in the theorem prover Isabelle/HOL.
    15 Type safety both of $micro$Java and the $micro$JVM
    16 are mechanically verified.
    17 
    18 To make the paper self-contained, it starts with
    19 introductions to Isabelle/HOL and the art of
    20 embedding languages in theorem provers.},
    21         CRClassification = {D.3.1, F.3.2},
    22         CRGenTerms = {Languages, Reliability, Theory, Verification},
    23         url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},
    24         pages = {117--144}
    25 }
    26 
    27 
    28 
    29 @inproceedings{DvO-ECOOP00,
    30         author = {David von Oheimb},
    31         title = {Axiomatic Semantics for {J}ava$^{\ell{}ight}$ in {Isabelle/HOL}},
    32         booktitle = {Formal Techniques for {J}ava Programs},
    33         year = {2000},
    34         publisher = {Fernuniversit{{\"a}t} Hagen},
    35         editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.},
    36         organization = {Technical Report 269, 5/2000},
    37         note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
    38         abstract = {We introduce a Hoare-style calculus for a nearly 
    39 full subset of sequential Java, which we call Java_light. In particular, 
    40 we present solutions to challenging features like exception handling, 
    41 static initialization of classes and dynamic binding of methods.
    42 
    43 This axiomatic semantics has been proved sound and complete w.r.t. 
    44 our operational semantics of Java_light, described in earlier papers.
    45 To our knowledge, our Hoare logic is the first one for an
    46 object-oriented language that has been proved complete.
    47 The proofs also give new insights into the role of type-safety.
    48 
    49 All the formalization and proofs have been done with the 
    50 theorem prover Isabelle/HOL.},
    51         CRClassification = {D.2.4, D.3.1, F.3.1},
    52         CRGenTerms = {Languages, Verification, Theory},
    53         url       = {\url{http://isabelle.in.tum.de/Bali/papers/ECOOP00.html}}
    54 }
    55 
    56 
    57 
    58 @inproceedings{KleinN00,
    59 author={Gerwin Klein and Tobias Nipkow},
    60 title={Verified Lightweight Bytecode Verification},
    61         booktitle = {Formal Techniques for {J}ava Programs},
    62         year = {2000},
    63         publisher = {Fernuniversit{{\"a}t} Hagen},
    64         editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.},
    65         organization = {Technical Report 269, 5/2000},
    66         note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
    67         url       = {\url{http://www4.in.tum.de/~nipkow/pubs/lbv.html}}
    68 }
    69 
    70 
    71 @article{KleinN-CPE01,
    72         author = "Gerwin Klein and Tobias Nipow",
    73         title = "Verified Lightweight Bytecode Verification",
    74         journal = "Concurrency and Computation: Practice and Experience",
    75         year = "2001",
    76         volume = "13",
    77         number = "13",
    78         editor = "Gary T. Leavens and Susan Eisenbach",
    79         pages = "1133-1151",
    80         url = {http://www4.informatik.tu-muenchen.de/~kleing/papers/cpe01.html},
    81         abstract = {Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual
    82 Machine code with types to enable a one-pass verification of welltypedness.
    83 We have formalized a variant of their proposal in the theorem prover
    84 Isabelle/HOL and proved soundness and completeness.},
    85         note = {Invited contribution to special issue on Formal Techniques for Java},
    86 }
    87 
    88 
    89 @inproceedings{Nipkow-FOSSACS01,author={Tobias Nipkow},
    90 title={Verified Bytecode Verifiers},booktitle=
    91 {Foundations of Software Science and Computation Structures (FOSSACS 2001)},
    92 editor={F. Honsell},publisher=Springer,series=LNCS,volume=2030,
    93 pages={347--363},year=2001}