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.
Type de document :
Rapport
[Research Report] RR-4047, INRIA. 2000, pp.53
Liste complète des métadonnées

Littérature citée [1 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00072591
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:21:20
Dernière modification le : samedi 27 janvier 2018 - 01:31:27
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:14:33

Fichiers

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

130

Téléchargements de fichiers

133