A Type System for Certified Binaries

Abstract

A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow safety rather than more advanced properties. In this paper, we present a general framework for explicitly representing complex propositions and proofs in typed intermediate and assembly languages. The new framework allows us to reason about certified programs that involve effects while still maintaining decidable typechecking. We show how to integrate an entire proof system (the calculus of inductive constructions) into a compiler intermediate language and how the intermediate language can undergo complex transformations (CPS and closure conversion) while preserving proofs represented in the type system. Our work provides a foundation for the process of automatically generating certified binaries in a type-theoretic framework.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2004
Accession Number
ADA436484

Entities

People

  • Bratin Saha
  • Nikolaos Papaspyrou
  • Valery Trifonov
  • Zhong Shao

Organizations

  • Yale University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Artificial Intelligence
  • Assembly Languages
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Language
  • Models
  • New York
  • Notation
  • Prime Numbers
  • Programming Languages
  • Recursive Functions
  • Semantic Models
  • Software Development
  • Standards

Fields of Study

  • Computer science

Readers

  • Computational Linguistics