[Apologies for multiple copies]
I am pleased to announce the 52nd Tokyo Programming Seminar, which will be held at NII on August 3 (Wed).
Janis Voigtlander from University of Bonn will give a talk about quantitative free theorems for reasoning runtime efficiency, and Zhenjiang Hu from National Institute of Informatics will give a talk about backward transformation determinization for bidirectional transformation.
The programme is attached below. I'm looking forward to meeting you at ToPS.
Best regards, Kazuyuki Asada
----
The 52nd ToPS http://www.ipl.t.u-tokyo.ac.jp/~tops/upcoming_seminar.html
Time: August 3rd (Wed) 2011, 15:00--17:00 Place: Rm. 1208, 12F, National Institute of Informatics Speaker: 1. Janis Voigtländer (Institute for Computer Science, University of Bonn)
Type-Based Reasoning about Efficiency
Abstract: Phil Wadler (1989) showed how to use John Reynolds' (1983) concept of relational parametricity to derive statements about programs in a purely functional language just from their (polymorphic) types. Such statements have found applications as so-called "free theorems". Traditionally, they have had an extensional flavor only: statements relating the value semantics of program expressions, but not statements relating their runtime (or other) cost. We present an extension of the technique that allows precisely statements of the latter flavor, by deriving quantitative theorems for free. Extending the underlying theory (of relational parametricity) is one thing, finding effective ways to do the actual deriving of concrete free theorems (by symbolic manipulations) is quite another, and more challenging here than in the standard/extensional cases.
2. Zhenjiang Hu (National Institute of Informatics)
Determinization of Backward Transformation
Abstract: Bidirectionalization is an automatic program transformation that derives a backward transformation from a given forward transformation. In general, more than one backard transformations exist and the problem is how to choose the "best" backward transformation that not only satisfies the roundtrip property but also meets the user's intention. I would like to discuss the importance of backward transformation determinization and explain some possible solutions.