@inproceedings{a73c85988273446dbb367a1a9e422358,
title = "A bytecode logic for JML and types",
abstract = "We present a program logic for virtual machine code that may serve as a suitable target for different proof-transforming compilers. Compilation from JML-specified source code is supported by the inclusion of annotations whose interpretation extends to non-terminating computations. Compilation from functional languages, and the communication of results from intermediate level program analysis phases are facilitated by a new judgement format that admits the compositionality of type systems to be reflected in derivations. This makes the logic well suited to serve as a language in which proofs of a PCC architecture are expressed. We substantiate this claim by presenting the compositional encoding of a type system for bounded heap consumption. Both the soundness proof of the logic and the derivation of the type system have been formally verified by an implementation in Isabelle/HOL.",
author = "Lennart Beringer and Martin Hofmann",
year = "2006",
doi = "10.1007/11924661_24",
language = "English (US)",
isbn = "3540489371",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "389--405",
booktitle = "Programming Languages and Systems - 4th Asian Symposium, APLAS 2006, Proceedings",
address = "Germany",
note = "4th Asian Symposium on Programming Languages and Systems, APLAS 2006 ; Conference date: 08-11-2006 Through 10-11-2006",
}