[TYPES] Paper: Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code

[Nadeem Abdul Hamid]

Dear Types readers,

We are pleased to announce the availability of our paper, "Interfacing 
Hoare Logic and Type Systems for Foundational Proof-Carrying Code." An 
abstract is below; the paper is available from:

http://flint.cs.yale.edu/flint/publications/rtpcc.html

Comments are most welcome.

--- Nadeem Abdul Hamid and Zhong Shao


Abstract

In this paper, we introduce a Foundational Proof-Carrying Code (FPCC) 
framework for constructing certified code packages from typed assembly 
language that will interface with a similarly certified runtime system. 
Our framework permits the typed assembly language to have a ``foreign 
function'' interface, in which stubs, initially provided when the 
program is being written, are eventually compiled and linked to code 
that may have been written in a language with a different type system, 
or even certified directly in the FPCC logic using a proof assistant. We 
have increased the potential scalability and flexibility of our FPCC 
system by providing a way to integrate programs compiled from different 
source type systems. In the process, we are explicitly manipulating the 
interface between Hoare logic and a syntactic type system.

To our knowledge, this is the first account of combining such 
certification proofs from languages at different levels of abstraction. 
While type systems such as TAL facilitate reasoning about many programs, 
they are not sufficient for certifying the most low-level system 
libraries. Hoare logic-style reasoning, on the other hand, can handle 
low-level details very well but cannot account for embedded code 
pointers in data structures, a feature common to higher-order and 
object-oriented programming. We outline for the first time a way to 
allow both methods of verification to interact, gaining the advantages 
of both and circumventing their shortcomings.