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.
1. Kazuyuki Asada (National Institute of Informatics)
Many-sorted Bialgebraic Semantics for a Multi-rooted Graph Algebra and a CBV Calculus
Abstract:
In this talk, bialgebraic semantics for the graph algebra introduced
by Buneman et al. is given.
The graph algebra is a graph representation for some kind of
multi-rooted graph, which is the same as Kripke model.
First I give a bijective correspondence between graph algebras and
terms in (the first-order part of) a call-by-value calculus
equipped with output, non-termination, non-determinism, and
iteration operator. Then I induce an equational theory for graph
algebra from the standard one for the CBV calculus including
(modified) uniformity for the iteration operator.
Then, after reveiwing coalgebraic semantics for Kripke model,
we see that those final coalgebras form a relative monad, and
the graph algebra can be formulated as many-sorted algebra.
Then I give many-sorted bialgebraic semantics for the graph
algebra and the graph.
Time permitting, I will explain three future works: Completeness
of the equational theory, full-abstractness, and generalization.
2. Shin-ya Katsumata (Kyoto University)
A Categorical Approach to Attribute Grammars
Abstract:
Attribute grammars (AGs) are a mechanism to assign computations with
bidirectional information flow to trees. We introduce a categorical
formulation of AGs called monoidal AGs, and demonstrate that they
subsume existing formulations of AGs, such as domain-theoretic,
graph-theoretic, and relational ones, and also a special class of
syntactic AGs called SSUR-ACs. Using this categorical formulation, we
give a syntax-free account of the descriptional composition, which
is a method to fuse two term transformation algorithms described by
SSUR-ACs into one.
1. Ichiro Hasuo (University of Tokyo)
Introduction to Coalgebra, through Final Sequences
Abstract:
In this talk I wish to deliver an elementary and informal introduction
to the theory of coalgebra---a mathematical machinery underlying
coinductive datatypes in functional programming---focusing on its
aspect of being the categorical dual to algebra. More specifically,
I'll first review the categorical "initial sequence" construction of
an initial algebra, and then elaborate on its dual--the "final
sequence" construction of a final coalgebra. A trip along these
sequences is a good way to familiarize ourselves with the essence of
induction and coinduction, and the contrast between them.
2. Yde Venema (University of Amsterdam)
Coalgebra Automata
Abstract:
Automata operating on infinite objects provide an invaluable tool
for the spcification and verification of programs. Many of the
infinite objects studied in this area, such as words/streams,
trees, graphs or transition systems, represent ongoing behaviour
in some way, and provide key specimens of coalgebras. Hence it
make sense to develop a universal theory of coalgebra automata:
automata operating on coalgebras. The motivation underlying the
introduction of coalgebra automata is to gain a deeper
understanding of this branch of automata theory by studying
properties of automata in a uniform manner, parametric in the
type of the recognized structures. Coalgebraic automata theory
thus contributes to Universal Coalgebra as a mathematical theory
of state-based evolving systems.
In the talk we give a quick introduction to coalgebra, and we introduce the notion of a coalgebra automaton. We will see that in fact a large part of the theory of parity automata can be lifted to a coalgebraic level of generality, and thus indeed belongs to the theory of Universal Coalgebra. More specifically, coalgebra automata satisfy various closure properties: under some conditions on the coalgebraic type, the collection of recognizable languages are closed under taking union, intersection, complementation, and existential projections. Time permitting, we will discuss two kinds of coalgebra automata, corresponding to approaches in coalgebraic logic that are based on, respectively, relation lifting and predicate liftings. Our results have many applications in the theory of coalgebraic fixpoint logics), but these will only be discussed tangentially.
Back to the top page