A type system for certified binaries
- 1 January 2005
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 27 (1) , 1-45
- https://doi.org/10.1145/1053468.1053469
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 article, 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.Keywords
This publication has 5 references indexed in Scilit:
- CPS Translations and Applications: The Cube and BeyondHigher-Order and Symbolic Computation, 1999
- A Syntactic Approach to Type SoundnessInformation and Computation, 1994
- Singleton, union and intersection types for program extractionPublished by Springer Nature ,1991
- The calculus of constructionsInformation and Computation, 1988
- Constructive Mathematics as a Programming Logic I: Some Principles of TheoryNorth-Holland Mathematics Studies, 1985