Write a Blog >>
PEPM 2017
Mon 16 - Tue 17 January 2017
co-located with POPL 2017
Mon 16 Jan 2017 16:00 - 16:30 at Salle 109, Barre 44-54 - Transformation (part I) Chair(s): Chung-chieh Shan

Dynamic code generation is useful for optimizing code with respect to information available only at run-time. Writing a code generator is, however, difficult and error prone. We consider a simple language for writing code generators and propose an automated method for verifying code generators. Our method is based on higher-order model checking, and can check that a given code generator can generate only closed, well-typed programs. Compared with typed multi-stage programming languages, our approach is less conservative on the typability of generated programs (i.e., can accept valid code generators that would be rejected by typical multi-stage languages) and can check a wider range of properties of code generators. We have implemented the proposed method and confirmed its effectiveness through experiments.