Authors
Zhong Shao, Bratin Saha, Valery Trifonov, Nikolaos Papaspyrou
Publication date
2002/1/1
Book
Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Pages
217-232
Description
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 typetheoretic …
Total citations
20012002200320042005200620072008200920102011201220132014201520162017201820192020202120222023202431714111371151312131
Scholar articles
Z Shao, B Saha, V Trifonov, N Papaspyrou - Proceedings of the 29th ACM SIGPLAN-SIGACT …, 2002