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.

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00: Transformation (part I)PEPM 2017 at Salle 109, Barre 44-54
Chair(s): Chung-chieh ShanIndiana University, USA
16:00 - 16:30
Verification of Code Generators via Higher-Order Model Checking
PEPM 2017
Takashi SuwaUniversity of Tokyo, Japan, Takeshi TsukadaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan, Atsushi IgarashiKyoto University
16:30 - 17:00
Interactive data representation migration: Exploiting program dependence to aid program transformation
PEPM 2017
Krishna NarasimhanGoethe University, Julia LawallInria/LIP6, Christoph ReichenbachGoethe University