Actions for Efficient Type Representation in TAL

Email RIS file
Bookmark
Report an Issue

Efficient Type Representation in TAL

Author
Chen, Juan
Published
October 2009.
Physical Description
1 electronic document
Online Version

Availability

I Want It
I Want It

Finding items...

Restrictions on Access
Unclassified, Unlimited, Publicly available.
Free-to-read Unrestricted online access
Summary
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.
Other Subject(s)
Collection
NASA Technical Reports Server (NTRS) Collection.
Note
Document ID: 20150004717.
Annual IEEE Symposium on Logic in Computer Science (LICS 2009) 11th-14th August 2009, Los Angeles, California, USA LOGIC IN COMPUTER SCIENCE (LICS 2009) 11th-14th August 2009, Los Angeles, California, USA ; 11-14 Aug. 2009; Los Angeles, CA; United States.
International Workshop on Proof-Carrying Code and Software Certification; 15 Aug. 2009; Los Angeles, CA; United States.
Proceedings of the Third International Workshop on Proof-Carrying Code and Software Certification; 3-12; NASA/CP-2009-215403.
Terms of Use and Reproduction
Copyright, Distribution under U.S. Government purpose rights.
View MARC record | catkey: 15415091