loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07)
Foundational Typed Assembly Language with Certified Garbage Collection
Shanghai, China
June 06-June 08
ISBN: 0-7695-2856-2
Chunxiao Lin, University of Science and Technology of China
Andrew McCreight, Yale University
Zhong Shao, Yale University
Yiyun Chen, University of Science and Technology of China
Yu Guo, University of Science and Technology of China
Type-directed certifying compilation and typed assembly language (TAL) aim to minimize the trusted computing base of safe languages by directly type-checking low-level ma- chine code. However, the safety of TAL still heavily relies on its safe interaction with the underlying garbage collector. Based on a recent variant of foundational proof-carrying code (FPCC), we introduce a general methodology for com- bining foundational TAL with a certified garbage collector. We demonstrate the practicality of this approach by link- ing a typical TAL with a conservative garbage collector. This includes proving the safety of the collector, the sound- ness of TAL, and the safe interaction between TAL programs and the garbage collector. Our work is fully mechanized in the Coq proof assistant and the certified programs can be shipped immediately as FPCC packages.
Citation:
Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, Yu Guo, "Foundational Typed Assembly Language with Certified Garbage Collection," tase, pp.326-338, First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), 2007
Usage of this product signifies your acceptance of the Terms of Use.