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

Displayed 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 Shan Indiana University, USA
16:00
30m
Talk
Verification of Code Generators via Higher-Order Model Checking
PEPM 2017
Takashi Suwa University of Tokyo, Japan, Takeshi Tsukada University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan, Atsushi Igarashi Kyoto University
16:30
30m
Talk
Interactive data representation migration: Exploiting program dependence to aid program transformation
PEPM 2017
Krishna Narasimhan Goethe University, Julia Lawall Inria/LIP6, Christoph Reichenbach Goethe University