[logic-ml] The 52nd ToPS [Aug 3]

[Kazuyuki ASADA]

[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.