The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Foundational Typed Assembly Language with Certified Garbage Collection

Last modified: Thu Jun 14 07:40:13 2007 GMT.

Authors

Chunxiao Lin
Andrew McCreight
Zhong Shao
Yiyun Chen
Yu Guo

Abstract

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 machine 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 combining foundational TAL with a certified garbage collector. We demonstrate the practicality of this approach by linking a typical TAL with a conservative garbage collector. This includes proving the safety of the collector, the soundness 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.

Published

  • In Proc. 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE'07), Shanghai, China, pages 326-335, June 2007. ©2007 IEEE Computer Society.
  • PDF [210k]
  • Coq implementation [70k]
  • Collector and mutator assembly [1.4k], runnable using SPIM

  • Copyright © 1996-2017 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon