Authors
Zhong Shao
Valery Trifonov
Bratin Saha
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 ACM Transactions on Programming Languages and
Systems (TOPLAS), 27(1), pages 1-45, January 2005.
©2005 ACM.