Rome

IFIP21
Main.TwoDotOneGroup, Main.TwoDotOneObserversGroup

%TOC%

---++ 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&ouml;fner
   * Zhenjiang Hu -- arriving with LH236 from Frankfurt, at 17:20 on Sunday; staying at Hotel Napoleon
   * Cezar Ionescu
   * [[Main/Patrik Jansson][Patrik Jansson]] -- arriving with KL3401: AMS -> FCO (Rome) on Sunday at 14.40. Staying at [[http://www.hotelpresidentrome.com/][Best Western Hotel President Rome]].
   * Johan Jeuring
   * Peter King
   * Andres L&ouml;h -- arriving with AZ0437, MUC->FCO on Sunday at 13:25; staying at Best Western Hotel President Rome.
   * [[Main/LambertMeertens][Lambert Meertens]]
   * Bernhard M&ouml;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.  
   * [[Main/JoseOliveira][Jose Oliveira]] -- arriving on TP852, OPO->FCO, Sunday 5-Fev, 12:50; staying at [[http://www.hotelaquaeductus.it][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&auml;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:
<br>
Maurizio Proietti, CNR-IASI, Viale Manzoni 30, 00185 Roma
(researcher of the National Research Council of Italy)
<br>
Valerio Senni, Rome Tor Vergata University, 00133 Roma
(researcher post-doc contract holder)
<br>
Emanuele De Angelis, University of Chieti-Pescara, 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, 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.

   $  _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. <p>General comments about presentations: make sure to present a *problem*. <p>Should we offer speakers less time than requested? This is at the chairman's discretion. <p>Proposal: next time we will start with 10 minute uninterrupted introductions by all people who want to present a talk. <p>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

   $ Main.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 [[http://www.veraonocampus.uminho.pt/ModuleLeft.aspx?mdl=~/Modules/Generic/GenericView.ascx&ItemID=26&Mid=223&lang=pt-PT&pageid=88&tabid=4][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 [[http://www.cs.uu.nl/wiki/bin/view/IFIP21/WeltenburgGermany#Technical_presentations][Weltenburg]] meeting; here are the [[http://www.di.uminho.pt/~jno/ps/vncampusjno.pdf][slides]] of July 2011 shown at the meeting.)

   $ Main.JeremyGibbons, _Unifying theories of programming with monads_ (Monday, February 6, 2012, 11:04): Purely functional programming languages are nice&mdash;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. <p> (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&mdash;and it has changed since then anyway. There is a related [[http://web.comlab.ox.ac.uk/publications/publication4877-abstract.html][paper]], joint work with Main.RalfHinze.)

   $ Nils Anders Danielsson, _[[http://www.cse.chalmers.se/~nad/publications/danielsson-2.1-68-talk.pdf][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.

   $ Main.FritzHenglein, _Dynamic symbolic computation for domain specific language implementation_ (Monday, February 6, 2012, 14:49): 

   $ Cezar Ionescu, _[[%ATTACHURL%/wg2.1-cezar.pdf][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.

   $ Main.JohanJeuring, _[[%ATTACHURL%/JJRome.pdf][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. 

   $ Main.AndresLoeh, _[[http://www.andres-loeh.de/IFIP-MCE.pdf][Parallelizing maximal clique generation in Haskell]]_ (Tuesday, February 7, 2012, 9:00): 
   
   $ Main.JoseOliveira, _[[http://www.di.uminho.pt/~jno/ps/wg21-68sl.pdf][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 (<nop>LAoP) is put forward as extension of the standard algebra of programming (<nop>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 <nop>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 [[http://www.springerlink.com/content/u0377206w2115687/?MUD=MP][paper]].)

   $ Main.DoaitseSwierstra,  [[%ATTACHURL%/IFIP-Rome-final.pdf][ _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, _[[http://www.cs.utoronto.ca/~hehner/PHP.pdf][Problems with the Halting Problem]]_ (Tuesday, February 7, 2012, 14:02)

   $ Lambert Meertens, _[[%ATTACHURL%/SoWhy.pdf][Proof of the Halting Problem]]_ (Tuesday, February 7, 2012, 15:02): 

   $ Main.ShinChengMu and Main.JoseOliveira, _[[%ATTACHURL%/WG_2.pdf][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.

   $ Main.ZhenjiangHu, _[[%ATTACHURL%/ZHURome.pdf][GTA, A Calculational Framework for Parallel Programming with <nop>MapReduce]]_ (Tuesday, February 7, 2012, 16:25): <nop>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 <nop>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 <nop>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.

   $ Main.AndrewBlack, _[[%ATTACHURL%/O-JDahlTalk.pdf][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. <p>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 &#8212; fifty years later &#8212; 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. <p>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.

   $ Main.WouterSwierstra, _Formal derivation of a Krivine machine_ (Wednesday, February 8, 2012, 9:00): 

   $ Buz Uzgalis, _[[%ATTACHURL%/Bzets.pdf][Compressing bit sets]]_ (Wednesday, February 8, 2012, 10:23): 

   $ Main.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&ouml;fner, _[[%ATTACHURL%/PHORome.pdf][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.<p> 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. 


   $ Main.BrunoOliveira, [[%ATTACHURL%/BOLSlides.pdf][ _Functional programming with structured graphs_ ]] (Thursday, February 9, 2012, 11:02): 

   $ Main.AlbertoPettorossi, [[%ATTACHURL%/APERome.pdf][ _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 &#8211; Naples 1837) can be found in http://www.readbookonline.net/readOnLine/49549/ (thanks to Bernhard Moeller).

   $ Main.BernhardMoeller, [[%ATTACHURL%/BMORome.pdf][ _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].<p> 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. <p>[1] J. Reynolds. Separation Logic, A Logic for Shared Mutable Data Structures. Proc. 17th Symposium on Logic in Computer Science. IEEE 2002, 55-74 <p>[2] H.-H. Dang, P. Höfner, B. Möller. Algebraic separation logic. J. Log. Algebr. Program. 80(6), 221-247 (2011)

   $ Main.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. 

   * [[%ATTACHURL%/PhotoIFIPome2012Sel01.zip]]
   * [[%ATTACHURL%/PhotoIFIPome2012Sel11.zip]]
   * [[%ATTACHURL%/PhotoIFIPome2012Sel20.zip]]
   * [[%ATTACHURL%/PhotoIFIPome2012Sel21.zip]]
   * [[%ATTACHURL%/PhotoIFIPome2012Sel22.zip]]

---++ Meeting information

---+++ Location

[[http://www.auditoriumantonianum.it][Auditorium Antonianum]] <br>
Viale Manzoni 1 <br>
00185 Roma <br>
Italy

---+++Registration and accommodation

The location of our meeting of February 6-10, 2012 is:<br>
Auditorium Antonianum<br>
Viale Manzoni 1,<br>
00185 Roma <br>
tel. + 39 06 45582593<br>
www.auditoriumantonianum.it<br>
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.<br>
Best,<br>
Alberto 

(Here is a [[http://maps.google.com/maps/ms?msid=214616630799599639600.0004b0ff5d957b5d6bdf1&msa=0&ll=41.891224,12.510939&spn=0.010239,0.021694][Google Map]] showing the Auditorium and the hotels -Jeremy.)

---------------------------------------
Hotel Bled<br>
Via Santa Croce in Gerusalemme, 40<br>
00185 Roma<br>
info@leonardihotels.com
<br>
Signora Valentina<br>
Refer to: Convegno IFIP febbraio 2012
---------------------------------------
Hotel Milton <br>
Via Emanuele Filiberto 155<br>
00185 Roma <br>
info@miltonroma.com
<br>
Signor Emanuele Tesfai<br>
Refer to: Convenzione IASI-CNR
---------------------------------------
Hotel Emona Aquaeductus <br>
Via Statilia 23,<br>
00185 Roma <br>
info@hotelaquaeductus.it
<br>
Refer to: Convegno IFIP-TorVergata
---------------------------------------
Hotel Napoleon<br>
Piazza Vittorio Emanuele II, 105,<br>
00185 Roma <br>
infobook@napoleon.it
<br>
Refer to: Convenzione Università Sapienza
---------------------------------------
Hotel President: <br>
Via Emanuele Filiberto 173,<br>
00185 Roma
---------------------------------------
Domus Sessoriana<br>
Piazza Santa Croce in Gerusalemme 10, <br>
00185 Roma
<br>
+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/featured-articles/getting-from-rome-fiumicino-airport-to-rome.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 Main.LambertMeertens, _[[%ATTACHURL%/X+Y.pdf][ALGOL X and ALGOL Y]]_ : Abstract.
   $ 16:37 Main.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 Main.JeremyGibbons, _[[%ATTACHURL%/algol.pdf][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: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.

-- Main.JohanJeuring - 21 Feb 2012