A type system for certified binaries
- 1 January 2002
- conference paper
- Published by Association for Computing Machinery (ACM)
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 frameworKeywords
This publication has 24 references indexed in Scilit:
- A dependently typed assembly languagePublished by Association for Computing Machinery (ACM) ,2001
- Principled scavengingPublished by Association for Computing Machinery (ACM) ,2001
- A certifying compiler for JavaPublished by Association for Computing Machinery (ACM) ,2000
- Flexible type analysisPublished by Association for Computing Machinery (ACM) ,1999
- Intensional polymorphism in type-erasure semanticsPublished by Association for Computing Machinery (ACM) ,1998
- Safe kernel extensions without run-time checkingPublished by Association for Computing Machinery (ACM) ,1996
- Typed closure conversionPublished by Association for Computing Machinery (ACM) ,1996
- A Syntactic Approach to Type SoundnessInformation and Computation, 1994
- Static dependent types for first class modulesPublished by Association for Computing Machinery (ACM) ,1990
- The calculus of constructionsInformation and Computation, 1988