A bytecode logic for JML and types

Lennart Beringer, Martin Hofmann

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 4th Asian Symposium, APLAS 2006, Proceedings
PublisherSpringer Verlag
Pages389-405
Number of pages17
ISBN (Print)3540489371, 9783540489375
DOIs
StatePublished - 2006
Externally publishedYes
Event4th Asian Symposium on Programming Languages and Systems, APLAS 2006 - Sydney, Australia
Duration: Nov 8 2006Nov 10 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4279 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference4th Asian Symposium on Programming Languages and Systems, APLAS 2006
Country/TerritoryAustralia
CitySydney
Period11/8/0611/10/06

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'A bytecode logic for JML and types'. Together they form a unique fingerprint.

Cite this