--- a/src/HOL/MicroJava/document/root.bib Fri Sep 15 18:36:50 2000 +0200
+++ b/src/HOL/MicroJava/document/root.bib Fri Sep 15 18:43:15 2000 +0200
@@ -1,9 +1,8 @@
-
@inproceedings{NipkowOP00,
author={Tobias Nipkow and Oheimb, David von and Cornelia Pusch},
title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},
booktitle = {Foundations of Secure Computation},
- series= {NATO Science Series F: Computer and Systems Sciences}
+ series= {NATO Science Series F: Computer and Systems Sciences},
volume = {175},
year = {2000},
publisher = {IOS Press},
@@ -29,13 +28,13 @@
@inproceedings{DvO-ECOOP00,
author = {David von Oheimb},
- title = {Axiomatic Semantics for Java_light in Isabelle/HOL},
+ title = {Axiomatic Semantics for {J}ava$^{\ell{}ight}$ in {Isabelle/HOL}},
booktitle = {Formal Techniques for {J}ava Programs},
year = {2000},
publisher = {Fernuniversit{{\"a}t} Hagen},
editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.},
organization = {Technical Report 269, 5/2000, Fernuniversit{{\"a}t} Hagen},
- note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}}
+ note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
abstract = {We introduce a Hoare-style calculus for a nearly
full subset of sequential Java, which we call Java_light. In particular,
we present solutions to challenging features like exception handling,
@@ -64,6 +63,6 @@
publisher = {Fernuniversit{{\"a}t} Hagen},
editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.},
organization = {Technical Report 269, 5/2000, Fernuniversit{{\"a}t} Hagen},
- note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}}
+ note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
url = {\url{http://www4.in.tum.de/~nipkow/pubs/lbv.html}}
}