- 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
- Shin-Cheng 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 5-Fev, 12:50; staying at Hotel Emona Aquaeductus; leaving on TP843, FCO->LIS, Friday 10-Feb, 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)
Maurizio Proietti, CNR-IASI, Viale Manzoni 30, 00185 Roma
(researcher of the National Research Council of Italy)
Valerio Senni, Rome Tor Vergata University, 00133 Roma
(researcher post-doc contract holder)
Emanuele De Angelis, University of Chieti-Pescara, Italy
(phd student: software model checking)
Organizational and administrative matters
Friday morning, February 10, 2012.
- 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, IASI-CNR, 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 correct-first-time symbolic expression.
- 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 middle-school 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 so-called Lawvere theories than to monads per se.
(This is the second half-talk 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 half-talk. 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 meta-analysis), 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, Ask-Elle, 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 glue-ing 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 re-factoring 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 data-intensive 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 generate-and-test 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 filter-embedding theorem helps to develop parallel programs in a systematic and incremental way. This is a joint work with Kento Emoto and Sebastian Fischer.
- AndrewBlack, Object-oriented 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 Ole-Johan Dahl hus at the University of Oslo.
Object-oriented programming is inextricably bound up with the pioneering work of Ole-Johan 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 object-orientation 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 non-strict 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 higher-order 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 self-organising wireless multihop ad-hoc 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 test-bed experiments, have the key limitations that they are very expensive, time consuming and non-exhaustive. 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 ``time-to-market'' 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 Ad-hoc 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)  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 .
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.
 J. Reynolds. Separation Logic, A Logic for Shared Mutable Data Structures. Proc. 17th Symposium on Logic in Computer Science. IEEE 2002, 55-74
 H.-H. Dang, P. Höfner, B. Möller. Algebraic separation logic. J. Log. Algebr. Program. 80(6), 221-247 (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.
Viale Manzoni 1
Registration and accommodation
The location of our meeting of February 6-10, 2012 is:
Viale Manzoni 1,
tel. + 39 06 45582593
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
(Here is a Google Map
showing the Auditorium and the hotels -Jeremy.)
Via Santa Croce in Gerusalemme, 40
Refer to: Convegno IFIP febbraio 2012
Via Emanuele Filiberto 155
Signor Emanuele Tesfai
Refer to: Convenzione IASI-CNR
Hotel Emona Aquaeductus
Via Statilia 23,
Refer to: Convegno IFIP-TorVergata
Piazza Vittorio Emanuele II, 105,
Refer to: Convenzione Università Sapienza
Via Emanuele Filiberto 173,
Piazza Santa Croce in Gerusalemme 10,
+39 06 7061534/35
What to bring
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/featured-articles/getting-from-rome-fiumicino-airport-to-rome.html
At the Antonianum you can access the internet. Information will be given at the meeting.
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.
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
- 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 Algol-68, 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
Followed by a banquet.
We will visit the Vatican Museum and the Sistine Chapel on Wednesday afternoon.
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:30-11:00)
- Lunch (served at the meeting place, the Auditorium Antonianum): 12:30-14:00
- Afternoon sessions - 14:00 to 17:30 (coffee break at 15:30-16:00)
Coffee breaks, lunch, excursion, and banquet are included in the registration fee.
- 21 Feb 2012