TwoDotOneGroup, TwoDotOneObserversGroup

Minutes

Participants

• Andrew Black
• Hendrik Boom
• Ernie Cohen
• Nils Anders Danielsson
• Jules Desharnais
• Jeremy Gibbons
• Georges Gonthier
• Fritz Henglein
• Patrik Jansson
• Johan Jeuring
• Annie Liu
• Andres Loeh
• Conor McBride
• Lambert Meertens
• Larissa Meinicke
• Bernhard Möller
• Shin-Cheng Mu
• Theo Norvell
• Bruno Oliveira
• Peter Pepper
• Alberto Pettorossi
• Tom Rothamel
• Wouter Swierstra
• Tarmo Uustalu
• Janis Voigtl\xE4nder
• David Wile

Organizational and administrative matters

Morning Friday, September 24, 2010.

Proxies

Ralf Hinze, Eiiti Wada, Jose Oliveira -> Jeremy Gibbons; Patrik Jansson -> Johan Jeuring.

Membership

These private matters are not recorded in the public version of the minutes.

Next meetings

The 67th meeting will take place in Iceland, in Reykjavik, May 23–27, 2011, organized by Graham Hutton and hosted by Luca Aceto. The meeting after that will probably be held in Rome, in Spring 2012; this year is the 50th anniversary of IFIP WG2.1, the first official meeting of which was held in Rome in 1962.

Formal resolutions

Resolution 1

We the people present at the 66th meeting of WG2.1 in Atlantic City do declare our gratitude to Ernie Cohen for his impeccable and thoughtful organ-ization. We have been extravagantly nourished, both mentally and physically; he really pulled out all the stops for us.

Resolution 2

The members of IFIP WG2.1 would like to acknowledge again the impact - both professional and personal - made on the Group by Bob Paige, who was a member until his death in 1999. It was Bob's idea to produce a book capturing what the Group has done and where it is going. After he died, this idea evolved into a tribute to Bob himself, recording his own research and his vision for the future. The resulting book Automatic Program Development, including personal contributions from friends and family as well as technical contributions documenting Bob's influence, was edited by Olivier Danvy, Fritz Henglein, Harry Mairson, and Alberto Pettorossi, and published by Springer in 2008. Copies were presented to Bob's widow Nieba and their children Jane and John at a dinner in Philadelphia on 22nd September 2010; we are very grateful that the family could come and join us for the ceremony.

Technical presentations in scheduled order

$ ShinChengMu, Approximation by Thinning (Mon Sep 20, 2010, 11:20): The fully polynomial-time approximation scheme (FPTAS) is a class of approximation algorithms that is able to deliver an approximate solution within any chosen ratio in polynomial time. By generalising Bird and de Moor's Thinning Theorem to a property between three orderings, we come up with a datatype-generic strategy for constructing FPTAS. The connection between greedy, thinning, and approximation algorithms can thus be seen as a series of generalisations. Components needed in constructing an FPTAS are often natural extensions of those in the thinning algorithm. Design of complex FPTASs is thus made easier, and some of the resulting algorithms turn out to be simpler than those in previous works.

$ PatrikJansson, Simple Pure Type System Examples (Mon Sep 20, 2010, 12:15): The concept of a Pure Type System (PTS) captures a large family of lambda calculi with a parametrised type system. Examples include all the systems of the lambda cube as well as a number of other related systems. This talk presents the PTS type system, a few examples and an abstraction theorem (which I presented in more detail at meeting 65 as "Parametricity for Dependent Types" - joint work with Jean-Philippe Bernardy and Ross Paterson).

$ George Gonthier, Modular theorem proving (Mon Sep 20, 2010, 15:21): No abstract provided yet.

$ Nils Anders Danielsson, Total parser combinators using mixed induction and coinduction (Mon Sep 20, 2010, 16:47): Parser combinators provide an elegant method for implementing parsers. However, most parser combinator libraries fail to guarantee that parsing will terminate. I talked about a library which provides such a guarantee.

The library's interface is similar to that of many other parser combinator libraries, with three main differences. One is that the interface clearly specifies which parts of the constructed parsers may be infinite, and which parts have to be finite, using dependent types and a combination of induction and coinduction; another is that the interface allows many forms of left recursion; and the last is that the parser type is unusually informative. For more info, see http://www.cs.nott.ac.uk/~nad/publications/danielsson-2.1-66-talk.html.

$ Tarmo Uustalu, Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction (Mon Sep 20, 2010, 17:55): We look at the operational semantics of languages with interactive I/O through the glasses of constructive type theory. Following on from our earlier work on coinductive trace-based semantics for While, we define several big-step semantics for While with interactive I/O, based on resumptions and termination-sensitive weak bisimilarity. These require nesting inductive definitions in coinductive definitions, which is interesting both mathematically and from the point-of-view of implementation in a proof assistant.

After first defining a basic semantics of statements in terms of resumptions with explicit internal actions (delays), we introduce a semantics in terms of delay-free resumptions that essentially removes finite sequences of delays on the fly from those resumptions that are responsive. Finally, we also look at a semantics in terms of delay-free resumptions supplemented with a silent divergence option. This semantics hinges on decisions between convergence and divergence and is only equivalent to the basic one classically.

We have fully formalized our development in Coq.

(Joint work with Keiko Nakata.)

$ JeremyGibbons, The Art of Effectful Reasoning (Tue Sep 21, 2010, 9:10): Purely functional programming languages are nice—they provide good tools for capturing programming abstractions, and good support for reasoning about those abstractions. But they are restricted to pure programs; so we use monads (and arrows, and idioms) to encapsulate impure effects within a pure framework. However, it is by no means clear how to carry the simple equational reasoning that works so well for pure programs over to impure ones.

I am offering two half-talks on approaches to addressing this problem. One (joint work with Richard Bird) attempts to exploit the higher-order naturality properties of structured recursion patterns for effectful programs, such as monadic map and idiomatic traverse. The other (joint work with Ralf Hinze) attempts to adapt Hoare-style pre- and post-conditions to imperative functional programming. The two talks have a common start but soon diverge.

(In the end, I only presented the first half-talk.)

$ Conor McBride, Pivotal pragmatism (Tue Sep 21, 2010, 11:17): No abstract provided yet.

$ Theo Norvell, A type system for generic imperative programs (Tue Sep 21, 2010, 15:38): The context is a system for calculational derivation of imperative programs. We would like to find type errors, without having to explicitly declare a type for each free state variable. This talk describes an approach to type inference for imperative commands and imperative specifications in which the type inferred for each command express the required constraints on the types of its free state variables. I use Haskell-style type checking with functional dependencies.

$ AnnieLiu, Programming and optimizing distributed algorithms (Tue Sep 21, 2010, 16:36): This talk describes a language for programming distributed algorithms, compilation of the language to generate actual implementations, and powerful optimizations that incrementalize expensive queries and remove unnecessary messages. The language does not embody new concepts but is powerful and simple for expressing distributed algorithms cleanly, free of implementation details. For example, Lamport's distributed mutual exclusion algorithm can be written in 30 lines, almost exactly like the pseudo code description of the algorithm, but with a precise semantics for execution. A best effort for programming this algorithm led to about 200 lines or more in C and Java, about 100 lines or more in Erlang and Python, and 90 lines in PlusCal, a nonexecutable specification language for specifying distributed algorithms (all numbers are without comments and empty lines). Our compilation method allows similar programs to be generated automatically. Our optimizations allow more efficient implementations to be derived systematically.

$ PeterPepper, Towards a mathematical Theory of garbage Collection. (Tue Sep 21, 2010, 17:54): Concurrent garbage collectors are notoriously difficult to implement correctly. Previous approaches to the issue of producing correct collectors have mainly been based on posit-and-prove verification or on the application of domain-specific templates and transformations. We show how to derive the upper reaches of a family of concurrent garbage collectors by refinement from a formal specification, emphasizing the application of domain-independent design theories and transformations. A key contribution is an extension to the classical lattice-theoretic fixpoint theorems to account for the dynamics of concurrent mutation and collection. Moreover, we also present a unified view of all kinds of garbage collectors; mark-and-sweep, copying, and reference-counting collectors.

$ Wouter Swierstra, Jeremy's problem (Wed Sep 22, 2010, 9:08): No abstract provided yet.

$ Wouter Swierstra, Machine-checked proof for Dutch National Flag (Wed Sep 22, 2010, 9:29): No abstract provided yet.

$ LarissaMeinicke, Probabilistic Program Annotations (Wed Sep 22, 2010, 10:59): For qualitative programs, pairs of predicates may be used to describe properties of programs. Such Hoare triples can be verified using the pioneering work of Floyd (1967), Dijkstra (1971) and Hoare (1969), by finding a valid program annotation. For quantitative (i.e. probabilistic) programs, pairs of real-valued functions may be used to describe program properties (Morgan, McIver 2005). How can such quantitative Hoare triples be verified? In this talk I discuss some of the difficulties encountered when attempting to define what a probabilistic program annotation is, and I propose a solution. I then discuss a way in which such probabilistic program annotations can be automatically generated. The method proposed finds "linear" forms of invariants for "linear" probabilistic programs. (This is joint work with JP Katoen, AK McIver and CC Morgan.)

$ JanisVoigtlaender, Strictification of Circular Programs (Wed 12:50, Thu Sep 23, 2010, 9:13): Circular functional programs (necessarily evaluated lazily) have been used as algorithmic tools, as attribute grammar implementations, and as target for program transformation techniques. Classically, Richard Bird showed how to transform certain multi-traversal programs (which could be evaluated strictly or lazily) into one-traversal ones using circular bindings. Can we go the other way, even for programs that are not (?) in the image of his technique? Yes we can, even for programs like Chris Okasaki's circular breadth-first numbering example, with fairly general program derivation techniques and a little help (joint work with Joao Paulo Fernandes, Joao Saraiva, and Daniel Seidel).

$ AndrewBlack, Programmer-friendly refactoring tools (Thu Sep 23, 2010, 10:06): Programs are more than text. We sometimes become so intoxicated by the power of textual formalisms that we forget the simple fact that programs are rich multi-dimensional abstractions for which linear text is but one representation, and not a particularly good representation for many tasks.

The overarching theme of this research is to develop and evaluate "multiview" program editing and exploration tools: tools that reveal the deep structure of programs by presenting them in multiple ways. However, any scientific evaluation must examine programmer performance on a particular task, and ascertain if the representation designed to assist in that task has actually achieved its goal.

In this talk I will survey recent work on refactoring tasks performed by myself and Prof. Emerson Murphy-Hill, a recent graduate from PSU. We noticed that, while refactoring is common, tools that semi-automate refactoring are under-utilized. The consequence is that refactoring is slower and more error-prone than it need be. We focussed on the improving the usability of refactoring tools as one way to increase their use. I will argue that usability is indeed a problem, and describe some of our tools and their evaluation. We conclude that programming tools should fit the way that programmers choose to work, rather than requiring that programmers adopt a new workflow in order to use the tools.

Here are the slides about Multiview and the slides about refactoring. The latter are pretty horrible because I don't know how to export animations stage-by-stage from PowerPoint. If you do, please tell me how!

$ TomRothamel, Automatic Incrementalization of Queries in Object-Oriented Programs (Thu Sep 23, 2010, 11:57-12:30, 14:13): High-level queries improve the clarity of programs and the productivity of programmers, but can come at a cost to program efficiency when expensive queries are computed repeatedly on slightly changed inputs. This talk describes a method for automatically generating incremental implementations of queries in object-oriented programs. These queries may be over objects, sets, tuples, and maps; and may contain aggregation and grouping constructs. The method generates maintenance code and invocation mechanisms for all updates that may affect the query results, ensuring that the results are computed correctly and efficiently even though object references may be aliased arbitrarily. Our method has been implemented and applied to a variety of problem domains.

$ BernhardMoeller, Formalization of feature-oriented programming (Thu Sep 23 2010, 15:02 ): No abstract provided yet.

$ AlbertoPettorossi, Proving Properties of Infinite Behaviours by Transformation of omega-Programs (Thu Sep 23 2010, 16:46): (by Valerio Senni, Maurizio Proietti, and Alberto Pettorossi) based on a paper presented at International Conf. on Logic Programs, Edinburgh, 2010. Various techniques have been proposed for proving properties of reactive system, i.e., systems with infinite behaviour, such as communication protocols, security protocols, and hardware controllers. Some of them are based on model checking using Buchi automata and omega-regular languages. We present (1) an extension of logic programs, called omega-programs, that can be used for defining predicates over infinite lists and specifying properties of reactive systems and, in general, properties of infinite sequence of events, and (2) a transformation-based methodology which allows us to verify properties of omega-programs using unfold/fold rules and, thus, it provides an alternative, easy mechanizable technique to the proof of properties of reactive systems.

$ BrunoOliveira, Monads, Zippers and Views, Virtualizing the Monad Stack (Fri Sep 24 2010, 11:10): This work aims at making monadic components more reusable and robust to changes by employing two new techniques for manipulating monad stacks, the monad zipper and monad views. The monad zipper is a monad transformer that creates virtual monad stacks by ignoring particular layers in the concrete stack. Monad views allow further virtualization by abstracting the concrete monad stack into a virtual monad stack, which presents itself with a more suitable interface to a particular component, and they also allow restricted access to monads in the stack. Furthermore, monad views can be used by components to provide a call-by-reference-like mechanism to access particular layers of the monad stack. By working with virtual stacks, requirements of components in terms of the monad stack shape no longer need to be literally reflected in the concrete monad stack, making these components more reusable and robust to changes.

Meeting information

Location

The 66th meeting of IFIP WG2.1 will be hosted by Ernie Cohen in Atlantic City, New Jersey (USA), from 19 to 24 September, 2010. Atlantic City is a seaside resort town, famous for its casinos, beaches, nightlife, and especially its boardwalk. The meeting venue has easy beach access, and (weather permitting) we will try to arrange extended lunch breaks to allow ample time to relax on the beach and swim in the ocean.

Note that ICFP will be held in Baltimore the following week (with Satellite events over the weekend); we will arrange group travel to Baltimore Friday evening for everyone going there.

Venue

The meeting will be held at the Chelsea Hotel. Dinners will be held at a variety of local restaurants, and our excursion will likely be to Philadelphia. We will also return to Philadelphia on Friday afternoon.

Registration and accommodation

Participants are expected to arrive on Sunday, September 19 and depart on Friday, September 24. To guarantee a room, please register by August 15. To register, send email to me (ernie.cohen@acm.org); please include your arrival and departure information, and if you are bringing extra guests.

The total cost of the conference should be around 800 euros or so. Please contact me (ernie) if this is a concern.

What to bring

Please be prepared to spend some time on the beach (though it is not mandatory), both in clothes (since we might eat at least one lunch on the beach) and in bathing suit (if you want to swim).

Travelling

Most travelers will prefer to fly into Philadelphia International Airport (PHL). From there, the simplest route is to take SEPTA train to 30th Street Station Philadelphia (about 20 min, $5), change to the Atlantic City train (about 100 min, $8)(schedule), and take a short taxi ride to the hotel. If you choose to rent a car at the airport, it is about a 70 min drive from PHL to the hotel. There are also minor variants possible if you plan to spend time in Philadelphia before or after; let me know if you plan to do this. We may arrange to shuttle some groups directly to the hotel from the airport.

Alternately, if you prefer to fly into New York, you can take the ACES train from New York Penn Station or Newark ($30-$40). On days where the ACES train doesn't run, you can take a train to Philadelphia and from there to Atlantic City. There are also busses available.

AC also has a small local airport (ACY) that might be suitable for some travelers, particularly those who happen to fly through Atlanta.

From the Baltimore/Washington area, there is bus service directly to Atlantic City, or you can take the train to Philadelphia and proceed as above.

Since almost everybody in the group is going to or through Philadelphia after the meeting, we will arrange transfer there after the meeting. The current plan is that after Friday lunch, we will all go to the Barnes Foundation in Philadelphia have an early group dinner in Philadelphia (except for those who have to catch early flights), and then those going to ICFP will proceed to Baltimore (it looks like train will be cheaper and quicker than chartering a bus). If you are staying over Saturday but not going to ICFP, you should book (or ask me to book) a room in Philadelphia.

Internet

Internet access will be available, both in all guestrooms and in the conference room (but not on the beach). Note, however, that there is a no-computers policy during presentations (except for the presenter, and the secretary for secretarial purposes).

Latest information

See notes about travel after the meeting.

Meeting programme

Schedule

We will start at 9:00 on Monday and finish around noon on Friday. Please arrange to be there for the whole meeting.

The default schedule is as follows:

• Breakfast: 8:00
• Morning sessions - 9:00 to 12:30 (coffee break at 10:30)
• Lunch: 12:30
• Afternoon sessions - 14:00 to 18:00 (coffee break at 16:00)
• Dinner: 19:30

Note, however, that with good weather, we might opt to extend the lunch break to allow for more time on the beach. We may also plan some after-dinner activities on the boardwalk.

-- ErnieCohen - 30 Jan 2010

• distPL.pdf: distPL.pdf

• distPL.pdf: distPL.pdf

• distPL.pdf: distPL.pdf