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.
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.
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.
|Case_for_Multiple_Views.pdf||manage||745 K||25 Sep 2010 - 21:01||AndrewBlack||"Pre-talk" about Multi-view Programing|
|Refactoring_Overview.pdf||manage||2 MB||25 Sep 2010 - 21:31||AndrewBlack||Images of my refactoring talk|
|distPL.pdf||manage||71 K||21 Oct 2010 - 06:11||AnnieLiu|
|wg21m66-jg.pdf||manage||113 K||21 Sep 2010 - 23:18||JeremyGibbons|