A Coq Formalization of a Type Checker for Object Initialization in the Java Virtual Machine

Yves Bertot 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We worked on a type system proposed in [11] to enforce a discipline for object initialization in the Java Virtual Machine language, to show how this type system could be implemented in the Coq proof and specification language. We used this description both to prove the theorems of [11] and to construct an effective verifier for this discipline.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072591
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:21:20 AM
Last modification on : Monday, September 3, 2018 - 10:56:02 AM
Long-term archiving on: Sunday, April 4, 2010 - 11:14:33 PM

Identifiers

  • HAL Id : inria-00072591, version 1

Collections

Citation

Yves Bertot. A Coq Formalization of a Type Checker for Object Initialization in the Java Virtual Machine. [Research Report] RR-4047, INRIA. 2000, pp.53. ⟨inria-00072591⟩

Share

Metrics

Record views

150

Files downloads

171