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.
Back to the top page