TwoDotOneGroup,
TwoDotOneObserversGroup
Minutes
Participants
 Andrew Black
 Nils Anders Danielsson
 Robert Dewar
 Jeremy Gibbons  arriving on LH1846 from Munich, at 16:35 on Sunday (well, that was the plan anyway  now due at 21:00 on LH1850); staying at Hotel Napoleon
 Walter Guttmann
 Rick Hehner (and Margaret Jackson)  staying at Hotel Napoleon
 Fritz Henglein
 Peter Höfner
 Zhenjiang Hu  arriving with LH236 from Frankfurt, at 17:20 on Sunday; staying at Hotel Napoleon
 Cezar Ionescu
 Patrik Jansson  arriving with KL3401: AMS > FCO (Rome) on Sunday at 14.40. Staying at Best Western Hotel President Rome.
 Johan Jeuring
 Peter King
 Andres Löh  arriving with AZ0437, MUC>FCO on Sunday at 13:25; staying at Best Western Hotel President Rome.
 Lambert Meertens
 Bernhard Möller
 ShinCheng Mu  arriving with KL1597 (FLIGHT CANCELLED]) from Amsterdam on Sunday 09:05. Staying at Hotel Bled. Leaving on KL1602, 13:05, Sunday 12th Feb.
 Bruno Oliveira  arriving with Allitalia (flight 159) on Sunday 14:05; staying at Hotel Emona Aquaeductus.
 Jose Oliveira  arriving on TP852, OPO>FCO, Sunday 5Fev, 12:50; staying at Hotel Emona Aquaeductus; leaving on TP843, FCO>LIS, Friday 10Feb, 18:45.
 Helmut Partsch
 Alberto Pettorossi
 Doaitse Swierstra  arriving with KL340, Sunday at 14.40, staying at Milton, leaving KL1608, Friday at 21:15
 Wouter Swierstra
 Robert Uzgalis
 Janis Voigtländer
 Eiiti Wada  arriving on AZ785 from Tokyo, 19:00 Sunday; staying at Hotel Milton Roma; leaving on AZ784 to Tokyo, 15:00 Saturday.
 Dave Wile (and Linn)
Local observers:
Maurizio Proietti, CNRIASI, Viale Manzoni 30, 00185 Roma
(researcher of the National Research Council of Italy)
Valerio Senni, Rome Tor Vergata University, 00133 Roma
(researcher postdoc contract holder)
Emanuele De Angelis, University of ChietiPescara, Italy
(phd student: software model checking)
Organizational and administrative matters
Friday morning, February 10, 2012.
 Membership
 These private matters are not recorded in the public version of the minutes.
 Formal resolution
 The members of WG2.1 and the observers present at the 68th meeting, in Rome  on the occasion of the 50th anniversary of the conception of the Group, also in Rome  wish to thank Alberto Pettorossi, Emanuele De Angelis, Valerio Senni and Maurizio Proietti of the University of Rome, IASICNR, for arranging a wonderful meeting in the Eternal City. We experienced the rich and sometimes curious traditions of a venerable institution, such as being in conclave for the purpose of voting, and the acquired taste of formal singing. We were privileged to have the opportunity to study masterpieces of correctfirsttime symbolic expression.
 CIPS
 We received congratulations from CIPS, Canada's Association of IT Professionals on our 50th anniversary.
 Next meetings
 The 69th meeting will be held in Ottawa, Canada, October 8 12, 2012. The 70th meeting will probably be held near Ulm, in Germany, in July 2013, organized by Helmuth Partsch.
 Lambert Meertens
 Should we embark on a language design project, and if so, what would be the aim of the language? With particular attention for the possibility of a language for presenting distributed algorithms, or a language for describing languages. We would then organize a tutorial, and some of the unsolved problems within the field.
 Scheduling procedure
 We have used a timer to give a presenter the time (s)he asked for, and stop the timer when (s)he interacts with the audience. What did you think about this? Reactions are positive.
General comments about presentations: make sure to present a problem.
Should we offer speakers less time than requested? This is at the chairman's discretion.
Proposal: next time we will start with 10 minute uninterrupted introductions by all people who want to present a talk.
Talks by local observers? Local observers can also propose a presentation, but they very seldom get a chance to talk. Maybe we should make this clear from the start? Reactions: local observers can also give a 10 minute presentation. If they use their 10 minutes well, the voting system helps them getting a chance to present their ideas in more detail.
This meeting is organized by Alberto Pettorossi with Emanuele De Angelis, Valerio Senni and Maurizio Proietti.
Technical presentations in scheduled order
 JoseOliveira, Haskell for teenagers (Monday, February 6, 2012, 10:05)
 A brief account of how Haskell is introduced as first programming language to middleschool prospective students who visit the University of Minho in the Verão no Campus initiative ("a Summer week in the campus"), every year in July. (Related to talk Towards "Middle School" MPC given in the Weltenburg meeting; here are the slides of July 2011 shown at the meeting.)
 JeremyGibbons, Unifying theories of programming with monads (Monday, February 6, 2012, 11:04)
 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'll present an axiomatic approach to doing so, which turns out to owe more to socalled Lawvere theories than to monads per se.
(This is the second halftalk that I proposed at Meeting 66, but which I didn't get round to presenting there; it doesn't depend essentially on anything in the first halftalk. I also proposed it at Meeting 67, but we ran out of time—and it has changed since then anyway. There is a related paper, joint work with RalfHinze.)
 Nils Anders Danielsson, Calculating bag equalities (Monday, February 6, 2012, 14:02)
 Two lists are "bag equal" if they are permutations of each other, i.e. if they contain the same elements, with the same multiplicity, but perhaps not in the same order. I plan to describe how one can define bag equality as the presence of bijections between sets of membership proofs. This definition has some nice properties:
 Many bag equalities can be proved using a flexible form of equational reasoning.
 The definition generalises easily to arbitrary unary containers, including types with infinite values, such as streams.
 By using a small variant of the definition one gets set equality instead, i.e. equality where neither multiplicity nor order matters. Similar variations give the subset and subbag preorders.
 The definition works well in mechanised proofs.
 FritzHenglein, Dynamic symbolic computation for domain specific language implementation (Monday, February 6, 2012, 14:49)

 Cezar Ionescu, Calculation and Communication (Monday, February 6, 2012, 16:34)
 "Vulnerability" is an important concept in global change studies. At the Potsdam Institute for Climate Impact Research (PIK), we have come up with a formal model of vulnerability, in order to compare different vulnerability assessments (a task called metaanalysis), but also in order to better structure and test the software used for these assessments. I'd like to present some aspects of this formalization which are hopefully relevant and / or entertaining to the other participants.
 JohanJeuring, AskElle, a Haskell tutor (Monday, February 6, 2012, 17:30)
 In this talk I give a demo of a tutor for Haskell. Using the tutor, students can incrementally develop a program, ask for hints at intermediate steps, and check that they are still on their way to a correct solution. I will also show what a teacher has to do to achieve particular behavior in the tutor.
 AndresLoeh, Parallelizing maximal clique generation in Haskell (Tuesday, February 7, 2012, 9:00)

 JoseOliveira, Towards a Linear Algebra of Programming (Tuesday, February 7, 2012, 11:03)
 This talk will address probabilistic functional programming. Probabilistic functions are half way between relations and functions; they express the propensity, or likelihood of ambiguous outputs. A basis for a Linear Algebra of Programming (LAoP) is put forward as extension of the standard algebra of programming (AoP) based on relations. If one restricts to discrete probability spaces, categories of matrices provide adequate support for this extension while preserving the reasoning style typical of the standard AoP). As illustration of calculating with probabilistic folds a simple example will be given in which the propagation of a fault injected is addressed quantitatively. (Developed further in the following paper.)
 DoaitseSwierstra, Merging parsers (Tuesday, February 7, 2012, 12:02)
 We present the internal workings of the "Merging and Permuting Parsercombinators", which combine two separate aspects from the old uulib library. We show how the types actually guide the glueing part of the code.
Rick Hehner,
Problems with the Halting Problem (Tuesday, February 7, 2012, 14:02)
 Lambert Meertens, Proof of the Halting Problem (Tuesday, February 7, 2012, 15:02)

 ShinChengMu and JoseOliveira, Programming from Galois Connections (Tuesday, February 7, 2012, 15:51)
 Problem statements often resort to superlatives such as in eg. ". . . the smallest such number", "...the best approximation", "...the longest such list" which lead to specifications made of two parts; one defining a broad class of solutions (the easy part) and the other requesting one particular such solution, optimal in some sense (the hard part). We introduce a binary relational combinator which mirrors this linguistic structure and exploits its potential for calculating programs by optimization. This applies in particular to specifications written in the form of Galois connections, in which one of the adjoints delivers the optimal solution. The framework encompasses refactoring of results previously developed by by Bird and de Moor for greedy and dynamic programming, in a way which makes them less technically involved and therefore easier to understand and play with.
 ZhenjiangHu, GTA, A Calculational Framework for Parallel Programming with MapReduce (Tuesday, February 7, 2012, 16:25)
 MapReduce, being inspired by the map and reduce primitives available in many functional languages, is the de facto standard for large scale dataintensive parallel programming. Although it has succeeded in popularizing the use of the two primitives for hiding the details of parallel computation, little effort has been made to emphasize the programming methodology behind. In this talk, we show that MapReduce can be equipped with a programming theory in calculational form. By integrating the generateandtest programing paradigm and semi rings for aggregation of results, we propose a novel parallel programming framework for MapReduce. The framework consists of two important calculation theorems, the shortcut fusion theorem of semi ring homomorphisms bridges the gap between specifications and efficient implementations, and the filterembedding theorem helps to develop parallel programs in a systematic and incremental way. This is a joint work with Kento Emoto and Sebastian Fischer.
 AndrewBlack, Objectoriented programming, challenges for the next fifty years (Tuesday, February 7, 2012, 17:21)
 This is a reprise of a talk that I gave in August 2011 at the scientific opening of the OleJohan Dahl hus at the University of Oslo.
Objectoriented programming is inextricably bound up with the pioneering work of OleJohan Dahl and Kristen Nygaard on the design of the Simula language at the Norwegian Computing Center, starting in the Spring of 1961. But object orientation, as it exists today — fifty years later — is the result of a complex interplay of ideas, constraints and people. Dahl and Nygaard would certainly recognize it as their progeny, but might also be amazed at how much it has grown up.
In this talk, we look at what objectorientation is, how it as evolved to become the dominant programming paradigm, and what it has to offer as we approach the challenges of the next fifty years of informatics.
 WouterSwierstra, Formal derivation of a Krivine machine (Wednesday, February 8, 2012, 9:00)

 Buz Uzgalis, Compressing bit sets (Wednesday, February 8, 2012, 10:23)

 WalterGuttmann, Lazy relational programming (Wednesday, February 8, 2012, 11:30)
 Stateful computations can be integrated into lazy functional programming languages. Let's go the other way round and have laziness in imperative programming languages. To this end, I give a relational model of nonstrict computations. The relations satisfy algebraic properties known from other models of imperative programs and laws about dependences in computations. Infinite data structures are supported. To facilitate their use in programs and in program reasoning, I provide a relational semantics for higherorder procedures, parameters, partial application, algebraic data types, pattern matching and list comprehensions.
 Peter Höfner, Formal methods for wireless mesh networks (Thursday, February 9, 2012, 9:01)
 Wireless Mesh Networks (WMNs) have gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, video surveillance and smart grids. WMNs are essentially selforganising wireless multihop adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. Traditional tools for evaluating and validating network protocol, such as are simulation and testbed experiments, have the key limitations that they are very expensive, time consuming and nonexhaustive. Our goal is to use formal languages and formal methods for the design, evaluation and verification of WMN routing protocols. In particular we want to reduce the ``timetomarket'' for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this overview talk I describe the importance of WMNs and present one of the leading protocols, the Adhoc on Demand Distance Vector (AODV) routing protocol. Moreover, I present formal methods used so far to model, analyse and verify AODV. This includes a language based on process algebra, fully automation by a matrix model and the use of model checkers.
 BrunoOliveira, Functional programming with structured graphs (Thursday, February 9, 2012, 11:02)

 AlbertoPettorossi, Synthesis of concurrent behaviours (Thursday, February 9, 2012, 13:44)
 (Joint work with Emanuele De Angelis and Maurizio Proietti) We address the problem of the automatic synthesis of concurrent programs within a framework based on Answer Set Programming (ASP). Every concurrent program to be synthesized is specified by providing both the behavioural and the structural properties it should satisfy. Behavioural properties, such as safety and liveness properties, are specified by using formulas of the Computation Tree Logic, which are encoded as a logic program. Structural properties, such as the symmetry of processes, are also encoded as a logic program. Then, the program which is the union of these two encoding programs, is given as input to an ASP system which returns as output a set of answer sets. Finally, each answer set is decoded into a synthesized program that, by construction, satisfies the desired behavioural and structural properties.
The translation of the "Infinito" poem by Giacomo Leopardi (Recanati, 1798 – Naples 1837) can be found in
http://www.readbookonline.net/readOnLine/49549/ (thanks to Bernhard Moeller).
 BernhardMoeller, Transitive separation logic (Thursday, February 9, 2012, 14:38)
 Separation Logic (SL) [1] extends Hoare logic by formulas that allow reasoning about linked object/record structures. The original version has also been extended to concurrent contexts. In this talk we concentrate on an algebraic formulation for the essential constructs of SL at the data structure level; an algebraic description of the control structure level has been given elsewhere [2].
Original SL uses as its central construct the separating conjunction P*Q that, roughly, expresses that P and Q hold, but within separate parts of the memory. Being separate here means that the sets of cells of both parts are disjoint. However, there may be links from one part to the other (sharing). For certain algorithms, however, sharing has to be excluded, which is not easily expressible in SL. We define a stronger notion of separation that takes transitive links into account. This is based on modal diamond operators and reflexive transitive closure, together with corresponding fixpoint induction principles. We use these to express reachability, which will form the basis of an algebraic derivation of garbage collection algorithms.
[1] J. Reynolds. Separation Logic, A Logic for Shared Mutable Data Structures. Proc. 17th Symposium on Logic in Computer Science. IEEE 2002, 5574
[2] H.H. Dang, P. Höfner, B. Möller. Algebraic separation logic. J. Log. Algebr. Program. 80(6), 221247 (2011)
 EiitiWada, J.C.Maxwell's Planimeter 1856 (Friday, February 9, 2012, 11:28)

Pictures from the meeting
Alberto took a number of pictures at the meeting. I'm including the zip files here for downloading.
Meeting information
Location
Auditorium Antonianum
Viale Manzoni 1
00185 Roma
Italy
Registration and accommodation
The location of our meeting of February 610, 2012 is:
Auditorium Antonianum
Viale Manzoni 1,
00185 Roma
tel. + 39 06 45582593
www.auditoriumantonianum.it
info@auditoriumantonianum.it
Here is the list of some hotels nearby.
In those hotel which have a "Refer to: xxx" field
I have been in person and you should make the reservation
by first sending an email message mentioning the xxx string.
Check the price they offer you and then make your booking.
I realized that in some hotels, by making the booking at this early time,
you can have a really good price, maybe even better that the
one expected because of the agreement with me.
(By the way, they did not tell me the exact price they were going to
offer you under our agreements.)
I hope that the booking procedure will not cause you any
big problem.
Best,
Alberto
(Here is a
Google Map showing the Auditorium and the hotels Jeremy.)
Hotel Bled
Via Santa Croce in Gerusalemme, 40
00185 Roma
info@leonardihotels.com
Signora Valentina
Refer to: Convegno IFIP febbraio 2012
Hotel Milton
Via Emanuele Filiberto 155
00185 Roma
info@miltonroma.com
Signor Emanuele Tesfai
Refer to: Convenzione IASICNR
Hotel Emona Aquaeductus
Via Statilia 23,
00185 Roma
info@hotelaquaeductus.it
Refer to: Convegno IFIPTorVergata
Hotel Napoleon
Piazza Vittorio Emanuele II, 105,
00185 Roma
infobook@napoleon.it
Refer to: Convenzione Università Sapienza
Hotel President:
Via Emanuele Filiberto 173,
00185 Roma
Domus Sessoriana
Piazza Santa Croce in Gerusalemme 10,
00185 Roma
+39 06 7061534/35
What to bring
Travelling.
The Antonianum Auditorium is located near to the metro stop "Manzoni" of the Metro Line A (red line).
In Rome there are two metro lines only: the blue one and the red one. They cross at the stop "Termini" (which
is underground the main Railways Termini Station).
A metro ticket (1 euro) allows you a metro run + any number of bus runs within 75 minutes from first boarding the metro or a bus.
Tickets may the bought at any metro station at a vending machine using coins (touch screen interface with instructions in English).
From Fiumicino airport you can take (1) the first class, direct train to Termini Station or (2) the train to Stazione Tiburtina and then from there
you take (2.1) the metro line B (Blue line) (direction Laurentina) to Termini and then (2.2) from Termini the metro line A to Manzoni (two stops, direction Anagnina).
All hotels I suggested are located near Manzoni stop.
From Fiumicino Airport you can take a taxi, but please take an official taxi and do not accept offer of people who may approach
you offering to take you to Rome.
More information in
http://www.italylogue.com/featuredarticles/gettingfromromefiumicinoairporttorome.html
Internet
At the Antonianum you can access the internet. Information will be given at the meeting.
Latest information
At the moment there are a few centimeters of snow on the ground in Rome (a rare event, indeed).
It may continue snowing during the weekend.
**The public transport strike announced for Monday 6th February has been revoked.
I hope to see you all safe and sound on Monday 9:00 at the Antonianum.
* In case of need here is my cell phone number +39 339 6272159 (home +39 06 4958742)
The registration fee is 300 (threehundred) euro. The form of payment and details of how to pay
the fee will be send to each of the participants by email.
Meeting programme
IFIP WG2.1 50th anniversary
At the meeting in Rome we will celebrate the 50th anniversary of IFIP WG2.1 on Thursday afternoon, February 9, 2012.
 16:00 LambertMeertens, ALGOL X and ALGOL Y
 Abstract.
 16:37 RobertDewar, Some reflection on WG 2.1 history, Moving away from Algol
 I was chairman of the group during a rather interesting period in its history when it had completed work on Algol68, and was in a "what now" mode. I will share some reminiscences of this period, and perhaps that can lead to an interesting "what next" discussion.
 17:00 JeremyGibbons, Algorithmic Languages and Calculi
 Abstract.
Followed by a banquet.
Excursion
We will visit the Vatican Museum and the Sistine Chapel on Wednesday afternoon.
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 schedule is as follows:
 Morning sessions  9:00 to 12:30 (coffee break 10:3011:00)
 Lunch (served at the meeting place, the Auditorium Antonianum): 12:3014:00
 Afternoon sessions  14:00 to 17:30 (coffee break at 15:3016:00)
Coffee breaks, lunch, excursion, and banquet are included in the registration fee.

JohanJeuring  21 Feb 2012