A Translation from Typed Assembly Languages to Certified Assembly Programming

Last modified: Mon Oct 16 05:39:27 2006 GMT.

Authors

Abstract

Typed assembly languages (TAL) and certified assembly programming (CAP) are two techniques for low-level verifications. TAL uses syntactic types and typing rules for program specification and reasoning, while CAP uses Hoare-style logic assertions and semantic subsumptions. They are suitable for different kinds of verification tasks. Previously, programs verified in either one of them can not interoperate freely with the other, making it hard to integrate them into a complete system. Moreover, the relationship between TAL and CAP lines of work has not been discussed extensively.

In this paper, we do so by presenting a translation from a TAL language to a CAP language. The translation involves an intermediate step of a ``semantic'' TAL language. To better illustrate our key points, all three languages share a same untyped machine. Thus the shape of the source language is slightly different from the original TAL's. Nevertheless, it supports polymorphic code, mutable reference, existential, and recursive types. The target language is an extension of XCAP, a recent CAP language, with support of logical recursive specifications and logical mutable reference, both require minimal changes to XCAP and its meta theory. Since we proved typing preservation for the translation, there is a clear path to link and interoperate well-typed programs from traditional certifying compilers with certified libraries by CAP-like systems.

Draft

Coq implementaion [30k]

colophon