1. Robert Glück (Department of Computer Science, University of Copenhagen)
An Experiment with the Fourth Futamura Projection
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
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
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.
1. Tachio Terauchi (Tohoku University)
Dependent Types from Counterexamples
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
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
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
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.