1. Robert Glück (Department of Computer Science, University of Copenhagen)
An Experiment with the Fourth Futamura Projection
Abstract:
We have experimentally validated the theoretical insight, that a
compiler generator is an Ershov generating extension of a program
specializer, by showing that an existing offline partial
evaluator can perform the fourth Futamura projection.
Specifically, an online and an offline partial evaluator for an
imperative flowchart language were transformed into two new
compiler generators. To date, all previous compiler generators
based on partial evaluation were either generated by
self-application or handwritten.
Presented at the Ershov Memorial Conference 2009.
2. Kazutaka Matsuda (University of Tokyo / JSPS Researcher)
Grammar-based Approach to Invertible Programs
Abstract:
Program inversion has many applications such as implementation of
serialization/deserialization and support for redo/undo, and has been
studied by many researchers. However, little attention has been paid
to these problems: how to characterize programs that are easy or hard
to invert and whether, for each class of programs, efficient inverses
can be obtained. In this talk, we present a new inversion framework
that we call grammar-based inversion. In grammar-based inversion,
a program is associated with an unambiguous grammar describing the
range of the program. The complexity of the grammar indicates how
hard it is to invert the program, while the complexity is related to
how efficient an inverse can be obtained.
1. Keigo Imai (Nagoya University)
Type inference for session types by Haskell type-level programming
Abstract:
Session types statically ensure that communications over a channel
proceed according to a protocol. In this talk, I will present an
implementation of session types in Haskell. A notable difference over
other implementations is that our implementation requires almost no
type annotation or term annotation in a source code, and at the same
time provides full functionality including channel-generation and
channel-passing. The key of the design is the indexing of de Bruijn
levels with channel variables. By indexing channel variables with
natural numbers, and at the same time by regarding a session type
environment as a list of types, session type inference can be reduced
to constraint solving on the list. Such scheme is implemented with
type classes and functional dependencies. We also discuss such
implementation techniques for type-level programming.
The following is a link to the library "full-sessions", available in hackage.
http://hackage.haskell.org/package/full-sessions
1. Tachio Terauchi (Tohoku University)
Dependent Types from Counterexamples
Abstract:
Motivated by recent research in abstract model checking, we present a
new approach for inferring dependent types. Unlike many of the
existing approaches, our approach does not rely on programmers to
supply the candidate (or the correct) types for the recursive
functions and instead does counterexample-guided refinement to
automatically generate the set of candidate dependent types. The main
idea is to extend the classical fixed-point type checking routine to
return a counterexample if the program is found untypable with the
current set of candidate types. Then, an interpolating theorem prover
is used to validate the counterexample as a real type error or
generate additional candidate dependent types to eliminate the
spurious counterexample. The process is repeated until either a real
type error is found or sufficient candidates are generated to prove
the program typable. Our system makes non-trivial use of ``linear''
intersection types to generate candidate dependent types in the
refinement phase.
2. Eiichiro Chishiro (The University of Tokyo)
To make pointer analysis practical: a compiler developer's perspective
Abstract:
I will talk about our ongoing work on pointer analysis for optimizing
compilers. The purpose of this work is to develop a pointer analysis
which may find a safe answer even if it has some bugs. As bugs in
conventional pointer analysis cause a compiler to generate incorrect
code, more robust, or bug-insensitive, pointer analysis is desired to
increase the reliability of the compiler. Currently, we do not have
satisfactory result. We show one such analysis which is more robust
but less precise than the conventional one.
1. Kazuhiro Inaba (The University of Tokyo)
The Complexity of Tree Transducer Output Languages
Abstract:
Macro tree transducers are a finite-state machine model of
tree-to-tree translations. They are motivated by syntax-directed
semantics of programming languages and recently have been applied
to other areas, such as XML processing or the fusion transformation
of functions.
The talk discusses the complexity of the output languages generated by compositions of macro tree transducers. Two results are shown: their membership problem is in DSPACE(n) and hence are context-senstive, and the class is NP-complete. The key idea of the proof is what we call the "garbage-free" normal form of macro tree transducers, which assures that the sizes of all intermediate trees during a computation are always less than the size of the final output tree.
2. Hui Song (Peking University)
Supporting Model-Driven Development of Runtime Architecture Infrastructures
Abstract:
When software systems are running, their environments and user
requirements are also changing. That forces us to monitor and adjust
the systems during runtime. We can do such runtime management work
more easily if we have an architecture model of the system (think
about a similar case for mending a house). Runtime architecture
infrastructures are key equipments to enable such architecture-based
runtime management. They automatically synchronize the states of
running software systems and their architecture models, so that people
or software agents can monitor and control the running system by
directly editing these architecture models.
There are many different types of systems and architecture models. That means people often face the work for developing such infrastructures. We provide a tool-set that supports people to develop runtime architecture infrastructures in a model-driven way. They do not need to write much code, but just write three MOF models and one QVT transformation (which are all mainstream modeling standards) to specify the infrastructure they need, and our tool-set can automatically generate the infrastructure for them.
In this talk, I will demonstrate architecture-based runtime management, using a small case. After that, I will present how our tool-set supports model-driven development of the infrastructures to support such cases. Finally, I will try to discuss about the distinction between the engineering solutions and the linguistic solutions, when we both want to liberate people from solving a problem repetitively.
Back to the top page