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,
11essentially by omitting everything but classes.
12The type system and semantics of this language
13(and a corresponding abstract Machine $micro$JVM)
14are formalized in the theorem prover Isabelle/HOL.
15Type safety both of $micro$Java and the $micro$JVM
16are mechanically verified.
17
18To make the paper self-contained, it starts with
19introductions to Isabelle/HOL and the art of
20embedding languages in theorem provers.},
21        CRClassification = {D.3.1, F.3.2},
22        CRGenTerms = {Languages, Reliability, Theory, Verification},
23        url = {\url{https://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 
39full subset of sequential Java, which we call Java_light. In particular, 
40we present solutions to challenging features like exception handling, 
41static initialization of classes and dynamic binding of methods.
42
43This axiomatic semantics has been proved sound and complete w.r.t. 
44our operational semantics of Java_light, described in earlier papers.
45To our knowledge, our Hoare logic is the first one for an
46object-oriented language that has been proved complete.
47The proofs also give new insights into the role of type-safety.
48
49All the formalization and proofs have been done with the 
50theorem prover Isabelle/HOL.},
51        CRClassification = {D.2.4, D.3.1, F.3.1},
52        CRGenTerms = {Languages, Verification, Theory},
53        url       = {\url{https://isabelle.in.tum.de/Bali/papers/ECOOP00.html}}
54}
55
56
57
58@inproceedings{KleinN00,
59author={Gerwin Klein and Tobias Nipkow},
60title={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
82Machine code with types to enable a one-pass verification of welltypedness.
83We have formalized a variant of their proposal in the theorem prover
84Isabelle/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},
90title={Verified Bytecode Verifiers},booktitle=
91{Foundations of Software Science and Computation Structures (FOSSACS 2001)},
92editor={F. Honsell},publisher=Springer,series=LNCS,volume=2030,
93pages={347--363},year=2001}
94