Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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 (Research report)
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072591
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 10:21:20 AM
Last modification on : Wednesday, October 26, 2022 - 8:16:43 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

71

Files downloads

140