Python 3000

I received the following letter from Greg Wilson.

To: Simon Peyton Jones, Phil Wadler, Guy Steele


Hope you don't mind mail out of the blue, but Guido van Rossum and others have started serious design work on Python 3000, a next-generation successor to Python:


Lots of interesting things are in the mix right now, from implementation
details to the semantics of generic functions/multi-methods. If you'd
like to chip in, your ideas and critiques would be very welcome.




Talk: Safraless Compositional Synthesis

Moshe Y. Vardi. 4pm Tuesday 18th April 2006.

[Phil's comment: Great talk! Vardi went through the formalism step by step, which made it possible for someone like me to follow along and get some understanding of the landscape and the results.]

In automated synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. In spite of the rich theory developed for system synthesis, little of this theory has been reduced to practice. This is in contrast with of model-checking theory, which has led to industrial development and use of formal verification tools. We see two main reasons for the lack of practical impact of synthesis. The first is algorithmic: synthesis involves Safra's determinization of automata on infinite words, and a solution of parity games with highly complex state spaces; both problems have been notoriously resistant to efficient implementation. The second is methodological: current theory of synthesis assumes a single comprehensive specification. In practice, however, the specification is composed of a set of properties, which is typically evolving -- properties may be added, deleted, or modified.

In this work we address both issues. We extend a Safraless synthesis algorithm, which avoids both Safra's determinization and parity-game solving. Technically, our algorithm reduces the synthesis problem to the emptiness problem of a nondeterministic Buechi tree automaton A. The generation of A avoids determinization, avoids the parity acceptance condition, and is based on an analysis of runs of universal co-Buechi tree automata. The clean and simple structure of A enables optimizations and a symbolic implementation. In addition, it makes it possible to use information gathered during the synthesis process of properties in the process of synthesizing their conjunction, enabling compositional synthesis.

Joint work with Orna Kupferman and Nir Piterman.


Talk: The Weird World of Bi-Directional Programming

Benjamin Pierce. 4pm Monday, 17th April 2006.

[Phil's comment: I had to miss the talk, but I discussed the content with Benjamin. Interesting to see how this is coming on, and that different groups have independently developed similar ideas. One of the competing ideas has a weaker well-formedness condition that looks more like an adjoint or Galois connection than like a bijection, that could be interesting. Benjamin says the next step is a type system for their data model. Their data model seems the same as that used by Buneman, Davidson, Fernandez, and Suciu for UnQL, which allows a nice form of fixpoint definition that doesn't work for XML. The fixpoints always converge if labeled children form a set, but not if they form a list or bag.]

Abstract. Programs generally work in just one direction, from input to answer. But sometimes we need a program to work in two directions: after calculating an answer, we want to UPDATE the answer and then somehow calculate backwards to find a correspondingly updated input. Of course, in general, a given update to the answer may not correspond to a unique update on the input, or to any at all; we need an "update translation policy" that tells us which updates can be translated and how to choose among translations when there are many possibilities. The question of how to determine such a policy has been called the VIEW UPDATE PROBLEM in the database literature.

Many approaches to this problem have been devised over the years; most have taken existing database query languages (such as SQL) as their starting points and then proposed ways of describing or inferring update policies. More recently, several groups have begun working to design entirely new languages in which programs are inherently bi-directional -- i.e., in which every program can be read from left to right as a map from inputs to answers and from right to left as (roughly) a map from updated answers to updated inputs. Moreover, bi-directionality in these languages is treated compositionally: each primitive works in both directions, and the two directions of compound programs can be derived from the two directions of their subcomponents.

This talk charts some interesting regions of the world of bidirectional programming and bi-directional language design, using as a touchstone our experiences at the University of Pennsylvania in the context of the Harmony project, where bi-directional languages -- one for transforming trees and another for relational data -- play a crucial role in the architecture of a universal data synchronizer.


Paper: Descriptive and Relative Completeness of Logics for Higher-Order Functions

By Kohei Honda, Martin Berger, and Nobuko Yoshida.

[Phil's comment: The program logic itself looks remarkably straightforward.]

Abstract. This paper establishes a strong completeness property of compositional program logics for pure and imperative higher-order functions introduced in earlier work by the authors. This property, called descriptive completeness, says that for each program there is an assertion fully describing the former’s behaviour up to the standard observational semantics. This formula is inductively calculable from the program text alone. As a consequence we obtain the first relative completeness result for compositional logics of pure and imperative call-by-value higher-order functions in the full type hierarchy.



Planet Haskell

Thanks to Antti-Juhani Kaijanaho for adding this blog to Planet Haskell, an accumulator for blogs of Haskell-related folk.


Labeling images with a computer game

L von Ahn, L Dabbish - Proceedings of the ACM CHI, 2004.
An innovative idea: a game that you play for fun, that as a side effect produces accurate labels for images on the web. If this game was played on the same scale as other moderately popular games, it would provide accurate labels for every image in Google images within six months. The game is not that widely played, but has produced 15 million labels within a couple of years.

You can play the game here: www.espgame.org.

This page is powered by Blogger. Isn't yours?