- Jeremy Gibbons (+)
- Johan Jeuring (+)
- Helmuth Partsch (+)
- Jose Oliveira (+)
- Conor McBride (+)
- Andres Löh (+)
- José Pedro Magalhães (+)
- Lambert Meertens (+)
- Bernhard Möller (+)
- Zhenjiang Hu (+)
- Fritz Henglein (+)
- Janis Voigtländer (+)
- Graham Hutton (+)
- Wouter Swierstra (+)
- Peter Höfner (+)
- Meng Wang (+)
- Roland Backhouse (+)
- Carroll Morgan (+)
- Tom Schrijvers (+)
- Nils Anders Danielsson (+)
- Patrik Jansson (+) has published some photos from the venue and the excursion
- Doaitse Swierstra (+)
- Bruno Oliveira (+)
- Alberto Pardo (+)
Organizational and administrative matters
Friday morning, July 5, 2013.
- These private matters are not recorded in the public version of the minutes.
- Formal resolution
- Next meetings
- The 71st meeting will probably be held in Berlin, probably March 24 - 28, 2014, organised by Peter Pepper. Robert Dewar proposes to organise a next meeting at his house in Vermont. We will see if we can organize the 72nd meeting around December 8 - 12, 2014. August 24 - 28, 2015 Patrik suggests to visit Göteborg, and May 16 - 20, 2016 Conor offers to organize a meeting in Scotland. After this 74th meeting we might go to Uruguay, Australia, or China. The 76th meeting might be held in the Netherlands.
Technical presentations in scheduled order
- Graham Hutton, Calculating a Compiler (Monday, July 1, 2013, 11:02)
- For a number of years I've been interested in the issue of compiler correctness, and have spoken about this a number of times at WG2.1. However, I never managed to do what I really wanted, which was to calculate a compiler. After many failed attempts over many years, and dissatisfaction with existing techniques, we finally worked out how to do it in clean and simple way, at least for simple languages. In this talk I'll explain how the technique works for a small language of arithmetic expressions. The talk is based upon joint work with Nils Anders Danielsson. (slides)
- Jose Pedro Magalhaes, Generic generic programming (Monday, July 1, 2013, 11:40)
- While Generic Programming (GP) promises to reduce code duplication, there is a lot of code duplication across GP libraries. In this talk we introduce yet another library for GP in Haskell... from which we can automatically derive representations for the most popular other GP libraries. Our work unifies many approaches to GP, and simplifies the life of both library writers and users.
- Conor McBride, Frank - a direct style of programming with effects (Monday, July 1, 2013, 14:01)
- No abstract provided.
- Lambert Meertens, Actually, it is very simple... (Monday, July 1, 2013, 15:02)
- This is a rerun of a talk I presented at Doaitse's retirement symposium. It is also an introduction to my next talk (UniFormal...).
- Roland Backhouse, Turing-tape games - a challenge in algorithmic problem solving (Monday, July 1, 2013, 16:00)
- No abstract provided.
- Jose Oliveira, Calculating risk in functional programming (Tuesday, July 2, 2013, 9:05)
- Interested in probabilistic risk analysis of functional programs, we exploit the adjunction between distribution-valued functions and column stochastic matrices; while the first are monadic and "good for programming", the latter are "good for calculation". This leads to a linear algebra of programming (LAoP) in Bird-Moor style whose laws enable one to transform and fuse probabilistic programs with each other, eg. by probabilistic-fold fusion. Because pairing is a weak product in the LAoP, the tricky bit is probabilistic mutual recursion. But laws such as eg. "banana split" still hold. (Joint work with Daniel Murta partly reported here.)
- Jeremy Gibbons, Accumulating Attributes (Tuesday, July 2, 2013, 09:55)
- I didn't get the chance to attend Doaitse's retirement symposium, but I did write a paper for it. I propose to take the opportunity to present it now. While I was writing up my DPhil thesis on tree accumulations many years ago, I visited the Netherlands, where Doaitse explained to me that what I was really writing about (although I didn't know it myself) was attribute grammars. In a sense, he was right, and his observation turned into my final chapter. But only in a rather ad-hoc way; I can now see how to express the relationship between attribute grammars and tree accumulations much more elegantly, and generically, using the notion of derivatives of datatypes.
- Meng Wang, FliPpr - A Prettier Invertible Printing System (Tuesday, July 2, 2013, 11:13)
- When implementing a programming language, we often write a parser and a pretty-printer. However, manually writing both programs is not only tedious but also error-prone; it may happen that a pretty-printed result is not correctly parsed. In this paper, we propose FliPpr, which is a program transformation system that uses program inversion to produce a CFG parser from a pretty-printer. This novel approach has the advantages of fi ne-grained control over pretty-printing, and easy reuse of existing efficient pretty-printer and parser implementations.
- Lambert Meertens, UniFormal - Towards a Unified Framework (Tuesday, July 2, 2013, 14:01)
- In the talk entitled "Actually, it is very simple..." I claim that it should be possible to integrate hard-core mathematics (as done using theorem provers or proof assistants), traditional declarative programming in a variety of paradigms, and program calculation seamlessly, combining them in a unified open framework that allows you to move between all these without encountering apparent borders. In this talk I present a proposal to WG2.1 to undertake a project to define a formalism providing such a unified framework.
- Fritz Henglein, Towards generic distributive sorting and searching (Tuesday, July 2, 2013, 16:01)
- Comparison-based sorting algorithms and search trees are easily made generic, that is applicable to user-defined types and orders, by abstraction over the comparison function used. This has arguably contributed to their popularity even though distributive (radix/trie-based) and hashing techniques often have superior performance for special datatypes, such as for machine integers and character strings. In this talk we show how to make distributive techniques generic by structural recursion over a class of order representations. This ultimately achieves a seemingly impossible combination - maximal representation independence (the result is a function of pairwise inequalities amongst the input elements) and worst-case linear-time performance. In particular, (static)
We identify strong naturality—commutativity with generalized filtering—as as a powerful property of stable sorting and show how it facilities equational correctness proofs relating generically defined sorting (LSD-radix, MSD-radix, trie construction/tree sort) functions to each other.
- Peter Höfner, Ad hoc routing in mesh networks using algebra (Tuesday, July 2, 2013, 16:57)
- At the meeting in Rome I gave an overview of formal modelling and analysis of routing protocols for wireless mesh networks (WMNs). Afterwards I was asked to present details about the methods used. This talk presents some more details about the algebra used to model main aspect of routing protocols.
- Tom Schrijvers, Zipping search trees (Wednesday, July 3, 2013, 9:01)
- For many years, Prolog’s nondeterminism has inspired functional programming (FP) researchers. Indeed, many FP solutions have been proposed to make Prolog’s depth-first search (DFS) more flexible. Unfortunately, none of the FP solutions carries over to actual Prolog systems because they do not take the limitations of the Prolog system architecture into account.
In this work we develop a new FP solution that addresses Prolog’s longstanding problem of inflexible DFS while taking the WAM architecture into account. With a wide array of core FP concepts (monads, algebras, qualified types, free monad transformers, coroutines and delimited continuations) we derive an effective Prolog implementation from a functional spec ification of a new zip operator for search trees. This solution is effective in Prolog because it exploits the Prolog system architecture. Moreover, it is very expressive because it is imparted with a core FP property, namely compositionality.
- Janis Voigtländer, Understanding Idiomatic Traversals Backwards and Forwards (Wednesday, July 3, 2013, 10:45)
- At the Ottawa meeting, Jeremy talked about reasoning about an effectful tree traversal in terms of its inverse. An open question was - Given a function implementing some effectful traversal strategy for some datatype, subject to certain laws imposed in the literature, and a backwards traversal function idiomatically obtained from the given one, does an inversion law (forwards and backwards traversal with effect functions f and g cancel out, over arbitrary structures, if f and g cancel out locally in a single step) hold as a derived consequence or does it have to be imposed as an additional law? We have since been able to answer the question, and more. The inversion law is indeed a consequence of the other laws from the literature. In the course of proving that it is, we have proved a theorem of wider appeal. It gives an exact characterization of the lawful traversals, via a canonical representation, which helps to answer further open questions and conjectures from the literature. (joint work with Richard Bird, Jeremy Gibbons, Stefan Mehner and Tom Schrijvers, submitted to the Haskell Symposium)
- Marcos Viera and Doaitse Swierstra, Compositional Compiler Construction (Wednesday, July 3, 2013, 11:35)
- As a follow-up on my suggestion in Rome to look at compositionallanguage definitions, I will present our solution to the LDTA tool challenge and show how we are able to define a a series of language extensions and associated tasks in a completely compositional way. We use a toolbox which is implemented as a couple of in Haskell embedded DSL's. The presentation contains a few slides of Haskell code, but definitely not too many; just to give you an impression of how things look like. The complete material covered in Marcos Viera's thesis.
- Nils Anders Danielsson, Correct-by-construction pretty-printing (Thursday, July 4, 2013, 9:02)
- I will present a new approach to correct-by-construction pretty-printing. The basic methodology is the one of classical (not necessarily correct) pretty-printing - users convert values to pretty-printer documents, and a general rendering algorithm turns documents into strings. The main novelty is that dependent types are used to ensure that, for each value, the constructed document is correct with respect to the value and a given grammar. Other parts of the development use well-established technology - the pretty-printer document interface is basically that of Wadler (2003), but with more precise types, and a single additional primitive combinator; and Wadler's rendering algorithm is used.
I have proved that if a given value is pretty-printed, and the resulting string parsed (with respect to the same, unambiguous grammar), then the original value is obtained. I make no guarantees about "prettiness".
- Alberto Pardo, Just Do It While Compiling! Fast Extensible Records In Haskell (Thursday, July 4, 2013, 9:43)
- The library for strongly typed heterogeneous collections HList provides an implementation of extensible records in Haskell. In HList, records are represented as linked lists of label-value pairs with a lookup operation that is linear-time in the number of ﬁelds. Using type-level programming techniques we develop a more efﬁcient representation of extensible records. We propose two encodings for extensible records that improve lookup at runtime without needing a total order on the labels. One of the encodings performs lookup in constant time but at a cost of linear time insertion. The other one performs lookup in logarithmic time while preserving the fast insertion of simple linked lists. Through staged compilation, the required slow search for a ﬁeld is moved to compile time in both cases. This is a joint work with Bruno Martinez and Marcos Viera (slides).
- Wouter Swierstra, The semantics of version control (Thursday, July 4, 2013, 14:09)
- No abstract provided.
- Bernhard Möller, Graph models for concurrency (Thursday, July 4, 2013, 15:11)
- We report on ongoing joint work with Tony Hoare, Georg Struth, Stephan van Staden and others. The starting point is the algebraic model of general concurrency presented in the so-called Concurrent Kleene Algebras (CKA). The aim with that was to unify phenomena such as non-interleaving (true concurrency) semantics, shared memory, channel-based communication, weakly-ordered memory access, unreliable communications, massively re-ordering program optimisers etc. This ambitious programme is still in exploration phase; there are no larger case studies yet.
The algebra centers around the two operators ; and | of sequential and concurrent composition. Additionally there are choice and finite and infinite iteration. Although a comprehensive and concise algebraic theory has been developed, more and more readers (including the original authors) are dissatisfied with the standard model of CKA. They feel that it is too abstract and cannot be used to model real programming languages. The reason is that it is only based on causal/temporal dependence, but lacks a convenient treatment of data flow. Moreover, its unorthodox view of assertions and Hoare triples is a difficulty for many people.
A number of remedies have been tried, however, so far without full success. One non-standard model reflects only interleaving semantics and hence does not cover true concurrency. There are some non-standard half-models which are closer to real programming languages, but lack some essential laws.
Still CKAs seem useful, in particular because of their very elegant treatment of rely-guarantee reasoning. Therefore a new quest for one or more more concrete and full models of CKA has started. In the talk we briefly review the original theory and the standard model as well as the rely-guarantee part. Then we present current ideas on a full model that also deals with data flow. Moreover we show how to embed standard Hoare triples as well as tests and modalities as known from standard semiring theory into it. Finally, we sketch a few aspects of the non-standard and half-models.
- Zhenjiang Hu, ``Putback'' is the Essence of Bidirectional Programming (Thursday, July 4, 2013, 16:46)
- We argue that ambiguity is essential and unavoidable for get-based bidirectional transformation and advocate that the synchronization strategy should not be hidden from programmers but considered from the start. We propose a novel approach to specifying so called well-behaved bidirectional programs by their backward transformations, capable of expressing all aspects of a bidirectional transformation completely, while retaining maintainability. We show that well-behaved bidirectional transformations are uniquely determined by their backward transformations and corresponding forward transformations can be obtained for free. (Joint work with Sebastian Fischer and Hugo Pacheco.)
The meeting will be held in Günzburg near Ulm, Germany, July 1-5, 2013.
The exact location of the meeting will be Schloss Reisensburg (Reisensburg castle).
D-89312 Günzburg / Donau
Telephone: +49 (0)8221 / 907-0
Reisensburg by Plane
The nearest international airports are Stuttgart and Munich, farther away is Frankfurt. The airports of Frankfurt, Stuttgart and Munich have train stations at the terminals. Take a train to Günzburg which is the nearest railway station to Reisensburg castle. Here you best take a taxi to the Reisensburg. The costs for the taxi shoud be around 8 Euro.
If you plan to fly to Munich or Stuttgart via Frankfurt, check whether taking a train directly from Frankfurt might be the faster alternative.
Reisensburg by Train
The nearest railway station is Günzburg. Here you best take a taxi to Schloss Reisensburg. The costs for the taxi shoud be around 8 Euro.
Reisensburg by Car
If you come by car we recommend to get to Günzburg on the Autobahn A8 (motorway).
The Way to the Reisensburg by Car via A8, Junction Günzburg:
- Leave the A8 at Junction Günzburg towards Günzburg (signposted)
- Stay on this road (B16) for about 3.3 km. Then, at the roundabout, take the 3rd exit onto Dillinger Straße/B10.
- Follow Dillinger Straße (that means turning left).
- After a few hundred metres later you turn left again, signposted Reisensburg (Reisensburger Strasse).
- This road leads into the village Reisensburg. When it ends in a junction you turn left according to a low mounted signpost labelled Intern. Institut Schloss Reisensburg.
- You should now see the castle of Schloss Reisensburg on top of the hill in front of you. Welcome to Schloss Reisensburg!
- Route on Google Maps
Reisensburg/Günzburg Tourist Information
Registration and accommodation
| Please fill in the registration form.
The deadline for registrations is Friday, April 26.
Accommodations on Schloss Reisensburg (costs per day, including all meals):
- single room: 105 ¤ or 109 ¤ (depending on availability)
- double room: 102 ¤ per person
On days without "normal" dinner (i.e. excursion, banquet, and maybe the day of departure) the prices will be 21.50 ¤ less (per day).
Please note that after a room has been booked, cancellation will cause a fee of at least 100 Euro depending on room type and date.
Accomodation and drinks outside the meeting (i.e. during lunch or dinner as well as in the evenings) are to be paid directly to Reisensburg castle (on the day of departure). They accept cash (Euros, of course), Visa-Card, Mastercard (no American Express!), and ATM Card (bank card).
Reisensburg provides free internet acces - in the rooms by ethernet cable (which can be obtained on demand at the registration desk) and by WLAN at all other places. You are encouraged to bring your laptop - in particular for communication to the world outside the castle. Of course, the rooms are equipped with telefones, but there is a rather high charge (60 cents/unit for phone calls). Note that there is a no-computers rule (which includes tablets and smartphones!) during talks.
- In case of emergency on the day of arrival, here are a few telefone numbers where you may try to get help (The numbers are for use within Germany, from outside Germany you first have to dial the country code 0049 and to then skip the leading 0):
- Schloss Reisensburg: 0731-5038000, 0731-5038011, 08221-9070
- Taxis in Günzburg: O8221-1717, O8221-1616, O8221-8181, O8221-4631
- Helmuth Partsch (home): 07347-4741
- Tobias Weck (member of my group who helps in the organization): 0173-7700464
- Extrapolating the experience of the past three months this year, the weather will be an erratic choice out of hot (more than 30° Celcius), nice (sunny, between 20° Celsius and 30° Celsius), acceptable (a mixture of sun and clouds, around 20° Celsius), and bad (rainy, below 20° Celcius). Although I am in favour of an angelic choice, you better be prepared for all possibilities.
- There is no dinner organized for Sunday, June 30. Also, there is no dinner available at Schloss Reisensburg. Instead, you may take a little walk (roughly half an hour) – or take a taxi, if you are lazy or tired – from Reisensburg to the city of Günzburg where there are several nice restaurants (detailed information can be found in the information package you receive upon arrival). This might be particularly interesting, because on Saturday and Sunday there is „Guentia-Fest“, a kind of city festival with life music and other attractions in the streets around the centre of Günzburg (a street map can be found in the respective tourist brochure in the information package).
We will start at 9:00 on Monday and finish at noon on Friday. Please arrange to be there for the whole meeting.
Monday, Tuesday, and Thursday, the schedule is as follows:
- session - 9:00 to 10:30
- coffee break - 10:30 to 11:00
- session - 11:00 to 12:30
- lunch - 12:30 to 14:00
- session - 14:00 to 15:30
- coffee break at 15:30 to 16:00
- session - 16:00 to 18:00
- dinner - 19:00 to ...
Will be announced.
Will be announced.
The exact costs will be announced.
- 20 Jun 2013