Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Efficient Type Representation in TAL

Juan Chen


Certifying compilers generate proofs for low-level code that guarantee safety properties of the code. Type information is an essential part of safety proofs. But the size of type information remains a concern for certifying compilers in practice. This paper demonstrates type representation techniques in a large-scale compiler that achieves both concise type information and efficient type checking. In our 200,000-line certifying compiler, the size of type information is about 36% of the size of pure code and data for our benchmarks, the best result to the best of our knowledge. The type checking time is about 2% of the compilation time.


Publication typeInproceedings
Published inWorkshop on Proof-Carrying Code and Software Certification (PCC'09)
> Publications > Efficient Type Representation in TAL