Certifying Run-time Code Generation

Run-time code generation (RTCG) improves performance by letting programmers dynamically generate special-purpose code to exploit run-time invariants. A certifying compiler is one that produces ourput that can be mechanically checked to have certain properties (in our case type safety). We have developed an infrastructure for certifying compilation supporting RTCG. Our system includes: All these tools are included in the TAL distribution, and have been used both under Linux and Windows.