The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

A Type System for Certified Binaries

Last modified: Sat Jan 19 06:40:38 2002 GMT.

Authors

Zhong Shao
Bratin Saha
Valery Trifonov
Nikolaos Papaspyrou

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.

Published

In Proc. 29th ACM Symposium on Principles of Programming Languages (POPL'02), Portland, OR, pages 217-232, January 2002. ©2002 ACM.

Copyright © 1996-2024 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page
colophon