Object initialization in the Java Virtual Machine

Yves Bertot

Projet Lemme -- INRIA Sophia-Antipolis

Abstract:
We worked on a type system proposed in a paper by Freund and Mitchell to enforce a discipline for object initialization in the Java Virtual Machine Language and implemented it in the Coq proof and specification language. We used this description both to prove theorems of the original paper and to construct an effective verifier for this discipline. Thanks to the extraction mechanism provided by Coq, we obtain a program in CAML that can be directly executed on sample programs.

Back to schedule.

Marieke Huisman

Last modified: Thu Dec 14 2000