Loading...
Please wait, while we are loading the content...
Similar Documents
Efficient type representation in tal
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Chen, Juan |
| Copyright Year | 2009 |
| Description | 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. |
| File Size | 252985 |
| Page Count | 10 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20150004717 |
| Archival Resource Key | ark:/13960/t77t2pb8j |
| Language | English |
| Publisher Date | 2009-10-01 |
| Access Restriction | Open |
| Subject Keyword | Computer Programming And Software Assembly Language Data Compression Knowledge Representation Metadata Data Processing Object-oriented Programming Machine Oriented Languages Certification Programming Languages Program Verification Computers Computer Programs Specifications Coding Proving Computer Information Security Compilers Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Article |
