Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2005
Accession Number
ADA436479

Entities

People

  • Nadeem A. Hamid
  • Zhong Shao

Organizations

  • Yale University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Assembly
  • Assembly Languages
  • Coding
  • Computer Languages
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Construction
  • High Level Languages
  • Instructions
  • Language
  • Machine Languages
  • Models
  • Programming Languages
  • Semantic Models
  • Specifications

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Parallel and Distributed Computing.