Sciweavers

Share
FMICS
2009
Springer

A Certified Implementation on Top of the Java Virtual Machine

10 years 3 months ago
A Certified Implementation on Top of the Java Virtual Machine
Abstract. Safe is a first-order functional language with unusual memory management features: memory can be both explicitly and implicitly deallocated at some specific points in the program text, and there is no need for a runtime garbage collector. The final code is bytecode of the Java Virtual Machine (JVM), so the language is useful for programming small devices based on this machine. As an intermediate stage in the compiler's back-end, we have defined the Safe Virtual Machine (SVM), and have implemented this machine on top of the Java Virtual Machine (JVM). The paper presents the certified implementation of the SVM on top of the JVM. We have used the proof assistant Isabelle/HOL for this purpose.
Javier de Dios, Ricardo Peña-Marí
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2009
Where FMICS
Authors Javier de Dios, Ricardo Peña-Marí
Comments (0)
books