TwoDotOneGroup,
TwoDotOneObserversGroup
Minutes
Participants
 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.
 Membership
 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, Turingtape 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 distributionvalued 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 BirdMoor style whose laws enable one to transform and fuse probabilistic programs with each other, eg. by probabilisticfold 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 adhoc 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 prettyprinter. However, manually writing both programs is not only tedious but also errorprone; it may happen that a prettyprinted 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 prettyprinter. This novel approach has the advantages of fi negrained control over prettyprinting, and easy reuse of existing efficient prettyprinter 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 hardcore 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)
 Comparisonbased sorting algorithms and search trees are easily made generic, that is applicable to userdefined types and orders, by abstraction over the comparison function used. This has arguably contributed to their popularity even though distributive (radix/triebased) 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 worstcase lineartime 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 (LSDradix, MSDradix, 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 depthfirst 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 followup 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, Correctbyconstruction prettyprinting (Thursday, July 4, 2013, 9:02)
 I will present a new approach to correctbyconstruction prettyprinting. The basic methodology is the one of classical (not necessarily correct) prettyprinting  users convert values to prettyprinter 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 wellestablished technology  the prettyprinter 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 prettyprinted, 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 labelvalue pairs with a lookup operation that is lineartime in the number of ﬁelds. Using typelevel 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 socalled Concurrent Kleene Algebras (CKA). The aim with that was to unify phenomena such as noninterleaving (true concurrency) semantics, shared memory, channelbased communication, weaklyordered memory access, unreliable communications, massively reordering 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 nonstandard model reflects only interleaving semantics and hence does not cover true concurrency. There are some nonstandard halfmodels 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 relyguarantee 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 relyguarantee 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 nonstandard and halfmodels.
 Zhenjiang Hu, ``Putback'' is the Essence of Bidirectional Programming (Thursday, July 4, 2013, 16:46)
 We argue that ambiguity is essential and unavoidable for getbased 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 wellbehaved bidirectional programs by their backward transformations, capable of expressing all aspects of a bidirectional transformation completely, while retaining maintainability. We show that wellbehaved 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.)
Meeting information
The meeting will be held in Günzburg near Ulm, Germany, July 15, 2013.
Location
The exact location of the meeting will be Schloss Reisensburg (Reisensburg castle).
Schloss Reisensburg
BürgermeisterJohannMüllerStraße 1
D89312 Günzburg / Donau
Germany
Telephone: +49 (0)8221 / 9070
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.
Timetable information:
Hint: 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.
Timetable information:
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.
Payment
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), VisaCard, Mastercard (no American Express!), and ATM Card (bank card).
Internet
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 nocomputers rule (which includes tablets and smartphones!) during talks.
Latest information
 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: 07315038000, 07315038011, 082219070
 Taxis in Günzburg: O82211717, O82211616, O82218181, O82214631
 Helmuth Partsch (home): 073474741
 Tobias Weck (member of my group who helps in the organization): 01737700464
 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 „GuentiaFest“, 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).
Meeting programme
Schedule
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 ...
Excursion
Will be announced.
Banquet
Will be announced.
Cost
The exact costs will be announced.

JeremyGibbons  20 Jun 2013