Reykjavik

IFIP21
Main.TwoDotOneGroup, Main.TwoDotOneObserversGroup

Note: the Wiki complains when you try to save your edits, but until now it does save them anayway.

---++!! IFIP WG2.1 Meeting, Reykjavik, Iceland, 23-27 May 2011

%TOC%

---++ Minutes

---+++ Participants

   * Roland Backhouse
   * Andrew Black (could not attend due to volcanic eruption)
   * Nils Anders Danielsson (could not attend due to volcanic eruption) 
   * Jules Desharnais
   * Jeremy Gibbons
   * Andy Gill
   * Georges Gonthier
   * Walter Guttmann
   * Rick Hehner
   * Zhenjiang Hu (could not attend due to volcanic eruption)
   * Graham Hutton
   * Patrik Jansson (could not attend due to volcanic eruption)
   * Johan Jeuring
   * Andres Loeh
   * Conor McBride
   * Lambert Meertens
   * Bernhard Moeller
   * Shin-Cheng Mu
   * Jose Oliveira
   * Alberto Pardo
   * Wouter Swierstra
   * Tarmo Uustalu
   * Janis Voigtländer

---+++ Organizational and administrative matters

Morning Friday, September 24, 2010.

   $  _Membership_ : These private matters are not recorded in the public version of the minutes.

   $  _Next meetings_ : The 68th meeting will be held in Rome, in Winter 2012, probably in the week of February 6; this year is the 50th anniversary of IFIP WG2.1, the first official meeting of which was held in Rome in 1962. Jeremy and Johan will try to organise an afternoon with talks, followed by a banquet, to memorise the event. The 69th meeting will be held in Canada, in October 2012.

   $  _Michel Sintzoff_ : Michel passed away last year. The group wrote the following paragraph for his obituary: <br/> <br/>Michel was the longest-serving and most faithful active member of WG2.1, and we have all felt his influence over the last 42 years. He had a rare combination of excellent insight in technical matters, a determination always to understand, and a knack for asking penetrating questions. Even when pointing out flaws or omissions in our work, he always did so in a very constructive way. It is thanks to Michel that the ALGOL 68 Revised Report was so much more readable than the original Report: the structured presentation of the Semantics, replacing the goto style of the original, is due to him, as is the use of predicates in the syntax, and their use to bring the semantic context conditions into the syntax. <br/> <br/>We all have fond memories of Michel from the many WG2.1 meetings we have shared. He was unfailingly kind and welcoming, especially to younger academics, and was without arrogance or pomposity. We always knew that we had arrived at the right place when we heard his joyous laughter emanating from the general vicinity of the bar &#8212; often in response to his own jokes, but they were worth it. Dave Wile recalls the meeting in Ameland, Holland, the week of 9/11, when he was giving the banquet speech: He always loved to tease and instigate trouble. We sat together at the banquet and as I began my speech, he saw that my notes were on my Palm Pilot. During the speech, he quietly changed the page so I had no idea where I was or what I was talking about. I certainly hope he retained that impishness right to the end. Michel was loved and respected by us all, and he will be sorely missed.<br/> <br/> This paragraph appears in [[http://dx.doi.org/10.1016/j.scico.2011.02.004][The humble humorous researcher: A tribute to Michel Sintzoff]].

   $  _A Wikipedia page for WG2.1_ : A Wikipedia page now exists: [[http://en.wikipedia.org/wiki/IFIP_Working_Group_2.1]].

   $  _New working groups_ : There is a proposal for an IFIP working group on programming language design, which has been discussed via email. There is a new IFIP working group 2.14 on service-based systems.

   $  _Scheduling procedure_ : Bernhard expresses two concerns: there is an unbalance between fp-like talks and other talks, and talks sometimes go on too long. We will try next time using a timer to give a presenter the time (s)he asked for, and stop the timer when (s)he interacts with the audience.

   $  _Presentation aspects_ : Please put the slides you present on the Wiki! Presenters often show code. Please prepare readable code/syntax, with enough whitespace around operators, enough space for formulas, etc.

   $  _Formal resolution_ : We heartily thank Graham Hutton and Luca Aceto for their perfect organisation of the 67th meeting of WG2.1 in Reykjavik. We were greeted with an effusive welcome, and enveloped in natural warmth - indeed, all our discussions took place in an environment named after the Goddess of Love. <br/> <br/> During our excursion we learned that much of our behaviour was already in place in Iceland a thousand years ago:  <br/> <br/> "The Law Speaker recited the laws in force, standing at the Law Rock. He recited one third of the body of laws each year, but recited the rules of procedure of the Althing itself at every session. At the Law Rock, important speeches were made regarding the affairs of those present; the podium was also open to all who wished to address the assembly. The position of the Law Speaker was highly prestigious; outside the sessions of the Althing, however, the Law Speaker had no formal power in society. But knowledge of the law clearly brought the Law Speaker and other chieftains considerable power in practice."

---+++ Technical presentations in scheduled order

   $ Main.GrahamHutton, _How To Be More Productive_ (Tuesday, May 24, 2011, 10:03): Streams, or infinite lists, have many applications in functional programming, and are naturally defined using recursive equations.  But how do we ensure that such equations make sense, i.e. that they actually produce well-defined streams?  In this talk we present a new solution to this problem, based upon the topological notion of contractive functions on streams.  In particular, we give a sound and complete representation theorem for contractive functions on streams, and show how this can be used to ensure that recursive stream equations are well-defined.  (Joint work with Mauro Jaskelioff; the slides are available [[http://www.cs.nott.ac.uk/~gmh/contractive.ppt][here]].)

   $ Main.JoseOliveira, _[[http://www3.di.uminho.pt/~jno/ps/wg21-67b-sl.pdf][What does curry(M) mean for M a matrix?]]_ (Tuesday, May 24, 2011, 11:10): Functional programmers and type theorists will be unanimous about the usefulness of Cartesian closed type structures offering _currying_ and _uncurrying_. Now, functions are special cases of relations and these in turn are special cases of matrices. So the question arises `does the _curry/uncurry_ isomorphism carry over to relations and arbitrary matrices'? Self-adjunctions arising from biproducts provide the answer and deliver, for free, the theory of vectorization which supports the (parallel) implementation of linear algebra kernels. This works provided one abandons the idea that matrices are "number containers" and develops a proper, polymorphic type system for linear algebra. (Joint work with H. Macedo,  cf. a [[http://www3.di.uminho.pt/~jno/ps/scp11.pdf][paper]] we have submitted on this topic.)

   $ Main.RolandBackhouse, _A Field of Type Isomorphisms_ (Tuesday, May 24, 2011, 13:57): Lawvere is credited with the famous remark that "seven trees are one". More formally, the property is that the set of shapes of seven binary trees is isomorphic to the set of shapes of single binary trees. The strategy used to prove this property has been modelled as a game with coins, called nuclear pennies. We briefly mention how we have exploited our understanding of the theory in order to invent a novel class of "replacement-set games" of which nuclear pennies is an instance. The main part of the presentation concerns a subsequent remark made by Lawvere in 2004 [1], namely that he was unable to establish certain isomorphisms between tree structures, and Blass has proved that it is indeed impossible. We show, nevertheless, that the isomorphisms he mentioned can be proven by the introduction of lists. In particular, we show that the set of shapes of a single binary tree is isomorphic to the disjoint sum of the unit type and the set of shapes of three binary trees, from which many other isomorphisms follow. (Note that the statement of this property does not involve lists, but the proof necessarily does.) Algebraically, Fiore has shown that the proof of Lawvere's remark is based on constructing a ring from a rig; our proof takes the construction one step further to constructing a field from a ring -- lists provide a mechanism for constructing a pseudo-inverse operator. The isomorphisms have been implemented in Haskell. <br/> [1] Left and right adjoint operations on spaces and data types, F.W.F. William Lawvere, Theoretical Computer Science 316 (2004) 105  111.
 
   $ Main.JohanJeuring, _[[%ATTACHURL%/JohanJeuringReykjavik.pdf][A Programming Tutor for Haskell]]_ (Tuesday, May 24, 2011, 15:03): At the Braga meeting I talked about using strategies to assess functional programs from first-year computer science students (here are the [[http://www.cs.uu.nl/wiki/pub/IFIP21/BragaPortugal/JohanJeuringBraga.pdf][slides]]). We have extended our assessment framework to a functional programming tutor that can give hints, show worked-out examples, and report errors. The tutor supports incrementally constructing/refining a program, until it is provable equivalent to a model solution. In this talk I want to discuss the ideas behind the tutor.

   $ Main.AndyGill, _Generating Implementations of Error Correcting Codes using Kansas Lava_  (Tuesday, May 24, 2011, 16:27): At the University of Kansas, we are using a Haskell library called Kansas Lava to support the development of a number of hardware implementations of High-performance High-rate Error Correcting Codes. Traditionally, high-level MATLAB implementations of error correcting codes inform hand-written VHDL solutions. Instead of writing our VHDL directly by hand, we added a number of intermediate checkpointing stages to our development process, all involving Haskell implementations of the error correcting codes. By constructing and invoking all the Haskell solutions under a single framework, and making assurance connections between them, we can have a semi-formal model, a high-fidelity bit accurate implementation, and VHDL code automatically generated from this implementation. This provides two benefits. First, assurance arguments can be selectively strengthened as required, because of the commonality between implementations. Second, architectural design decisions can be postponed until after the semi-formal model is constructed, then explored with basic assurance infrastructure providing evidence of correctness. We report on our experiences using Kansas Lava, our research tool for supporting systems generation, and how it supported the development of our FPGA implementation of an existing NASA JPL Low-Density Parity-Check (LDPC) error correcting code.

   $ Main.ShinChengMu, _Generalising and Dualising the Third List-Homomorphism Theorem_ (Tuesday, May 24, 2011, 17:27):  The third list-homomorphism theorem says that a function is a list homomorphism if it can be described as an instance of both a foldr and a foldl. We prove a dual theorem for unfolds and generalise both theorems to trees; if a function generating a list can be described both as an unfoldr and an unfoldl, the list can be generated from the middle, and a function that processes/builds a tree both upwards and downwards may independently process/build a subtree and its one-hole context. The point-free, relational formalism helps to reveal the beautiful symmetry hidden in the theorem. (Joint work with Akimasa Morihata and Main.ZhenjiangHu.)

   $ Main.JeremyGibbons, _Maximum Segment Sum, Monadically_ (Wednesday, May 25, 2011, 09:01): It's an oldie, but a goodie. In their paper [[http://dx/doi.org/10.1017/S0956796800001556][Generic functional programming with types and relations]], Bird, de Moor, and Hoogendijk presented a relational calculation of a solution to the datatype-generic version of the maximum segment sum problem. Since I've had monads on the brain recently, I revisited this calculation from that perspective, and in doing so I [[http://patternsinfp.wordpress.com/2011/05/05/horners-rule/][learnt something interesting]] (at least to me) about the relational approach. In case the group is equally interested in this blast from the past, I'll tell the story.

   $ Main.JanisVoigtlaender, _[[%ATTACHURL%/jv-slides.pdf][Improvements for Free]]_ (Wednesday, May 25, 2011, 10:05): "Theorems for Free!" is a slogan coined by Phil Wadler (FPCA 1989) for a technique that allows to derive interesting statements about pure functions just from their (polymorphic) types. Such statements have always had an extensional flavor only; statements relating the value semantics of program expressions, but not statements relating their runtime (or other) cost. We present an extension of the technique that allows precisely statements of the latter flavor, by deriving quantitative theorems for free. Extending the underlying theory (of relational parametricity) is one thing, finding effective ways to do the actual deriving of concrete free theorems (by symbolic manipulations) is quite another, and more challenging here than in the standard/extensional cases. <p> (This is joint work with Daniel Seidel, presented at the Workshop on Quantitative Aspects of Programming Languages 2011. The paper version submitted to the workshop post-proceedings is [[http://www.iai.uni-bonn.de/~jv/qapl11.pdf][here]].) 

   $ Main.WouterSwierstra, _[[http://www.cs.ru.nl/~wouters/Talks/Refinement.pdf][Dependent types, predicate transformers, and refinement]]_ (Wednesday, May 25, 2011, 11:32): I would like to talk about ongoing work to embed a refinement calculus in a dependently typed programming language such as Agda or Coq. Instead of postulating the usual refinement laws, I will show how to define predicates and predicate transformers, and use these definitions to model the semantics of a small imperative language. The refinement laws then become derivable from this semantics, instead of being axioms.

   $ Main.AndresLoeh, _Expanding the universe_ (Wednesday, May 25, 2011, 12:08): Abstract not supplied.

   $ Main.AlbertoPardo, _Applicative Shortcut Fusion_ (Thursday, May 26, 2011, 09:33): Applicative functors, introduced by McBride and Paterson, provide a model of computational effects which generalise monads, but they favour an applicative programming style. In this talk we analyse shortcut fusion in the context of applicative computations. We provide a shortcut fusion rule for the  elimination of intermediate data structures generated in applicative computations. Our rule exhibits, once more, the relevance and generality of _traverse_, a datatype-generic operator for defining traversals over data structures where, like a _map_ function, an applicative action is applied to each element of a structure, threading the effects. Associated with the fusion rule, we introduce two combinators, _ifold_ and _ibuild_, which model the uniform consumption and production of data structures under applicative computations. (Joint work with German Delbianco and Mauro Jaskelioff, presented at TFP 2011).

   $ Main.ConorMcBride, _Tomorrow is Another Day_ (Thursday, May 26, 2011, 10:40): Circular programs always make my head spin, and sometimes my computer too. Lazy evaluation allows us to trade in data which do not yet exist, in the hope that they can be computed just in time. If an apparently circular program does not, in fact, have cyclic data dependencies, it will work! However, it is only too easy to write well-typed programs which consume data before they are produced and spiral into a black hole. This talk presents a typed approach to circular programming, abstractly modelling relative time, ensuring that the present does not depend on the future. Classic perplexing examples, such as repMin, and even the breadth-first tree-labelling algorithm of Jones and Gibbons are explicable in this setting, with a minimum of fuss. There is more than a hint of a connection with modal logic.
  
   $ Walter Guttmann, _Towards an Algebra of Computing_ (Thursday, May 26, 2011, 11:37): Already basic sequential systems have many different models with varying degrees of precision, for example, regarding their ability to distinguish normally terminating, non-terminating and aborting executions. Let's use algebra for giving structure to this diversity of models and for unifying existing approaches. I'll axiomatise the non-terminating executions of a system so as to derive complex results (while-program normal form theorem, connection between approximation and refinement fixpoints) which hold in several models. So far this is about relational, not trace-based models.

   $ George Gonthier, _How to make ad hoc proof automation less ad hoc_ (Thursday, May 26, 2011, 14:07): No abstract provided.

   $ Main.TarmoUustalu, _Reasoning about correctness of software transactional memory_ (Thursday, May 26, 2011, 14:55): It is a subtle task to state what it means for an implementation of software transactional memory to be correct, not to speak of proving it. We have stated and proved correctness of a particular implementation of software transactional memory for the While language extended with parallelism and (nested) transactions by reasoning about two  small-step operational semantics and an alignment relation between them. We have fully formalized the development in Agda. (Joint work with Andri Saar.)

   $ Main.BernhardMoeller, _A Survey of Product Family Algebra_ (Thursday, May 26, 2011, 16:33): We develop an algebra of product families with + standing for union and . for composition, like e.g. in regular expressions. There are distributive laws that allow factoring out commonality and, conversely, algebraically calculating all possible products in a family. The algebra is enriched by a relation expressing that presence of one feature necessitates or excludes that of another one. Finally the "syntactic" view working only with feature names is supplemented by a semantic one, in which features are programs with a soundly defined semantics, in such a way that the  axioms of product family algebra are still satisfied. (Joint work with Peter Höfner and Ridha Khedri)

   $ Main.ConorMcBride, _Kleisli Arrows of Outrageous Fortune_ (Friday, May 27, 2011, 11:50): Monads provide a type discipline for effectful programming, mapping value types to computation types. If we index our types by data approximating the &#8216;state of the world&#8217;, we refine our values to witnesses for some condition of the world. Ordinary monads for indexed types give a discipline for effectful programming contingent on state, modelling the whims of fortune in way that Atkey&#8217;s indexed monads for ordinary types do not (Atkey, 2009). Arrows in the corresponding Kleisli category represent computations which reach a given postcondition from a given precondition; their types are just specifications in a Hoare logic!

---++ Meeting information

---+++Schedule

The meeting will be held at Reykjavik University in Iceland, from
Monday 23rd May to Friday 27th May 2011.  The meeting will start
at 09.00 on Monday morning, and end after lunch on Friday at around 2pm. 
Participants are expected to stay for the whole meeting.  Most people will
wish to arrive on Sunday, and leave on Friday afternoon/evening or
on Saturday.  You may also wish to extend your stay by a day or two
either side of the meeting to do some additional sightseeing on your own.

The standard daily schedule is as follows:

09.00 - 10.30 : Talks<BR>
10.30 - 11.00 : Coffee<BR>
11.00 - 12.30 : Talks<BR>
12.30 - 14.00 : Lunch<BR>
14.00 - 15.30 : Talks<BR>
15.30 - 16.00 : Coffee<BR>
16.00 - 18.00 : Talks<BR>

There will be an excursion on Wednesday afternoon (14.00 - 20.30, departing from the University),
and a conference dinner on Thursday evening (19.30 at [[http://www.hofnin.is][Höfnin Restaurant]].)

---+++Location

The meeting will be held in room _Betelgaus is V.1.02_  on the ground floor of
the new Reykjavik University building, whose address is as follows:

Reykjavik University<BR>
Menntavegur 1<BR>
IS 101 Reykjavik

A shuttle bus from H&oacute;tel Fr&oacute;n to the Univesity will be
provided each morning during the meeting.  The shuttle will make two journeys
from the hotel, leaving at *08.15* and *08.35* each morning, and the journey
to the University takes around 10 minutes.  A member of staff will meet the shuttle
on Monday morning to show everyone the way to the meeting room.

---+++Registration

Please [[http://frontpage.simnet.is/ipg/ifipwg21reg.asp][register]] as soon as
possible, as the rooms at the hotel are only guaranteed until *29th April 2011*.

The all-inclusive cost is 118700 ISK (approx 641 GBP,
734 EUR, 1041 USD), which includes registration, 5 nights single
accommodation with breakfast, daily coffee and lunches, morning
shuttle to the university, excursion and conference dinner.
The registration form also allows participants to purchase extra
hotel nights, extra excursion and dinner tickets, and to select
different room options (single, double, sharing.)  Payment
can be made by bank transfer or credit card.

---+++Accommodation

Rooms at a discounted rate have been reserved in [[http://www.hotelfron.is/][H&oacute;tel Fr&oacute;n]], which
is located in the centre of Reykjavik on its main street, and can be
booked as part of the registration process.  The address and contact details of the hotel are as follows:

H&oacute;tel Fr&oacute;n<br>
Laugarvegur<br>
101 Reykjavik<br>
Phone: +354 511 4666<br>
Email: info@hotelfron.is

---+++Travel

Reykjavik's main airport is [[http://www.kefairport.is/english/][Keflavik International Airport]]
(KEF) and is served by many international hubs.  It should be
possible for most participants to fly to Keflavik directly or
with a single change.  Iceland is a popular tourist destination,
so please book your flights as soon as possible.

The [[http://www.re.is/Flybus/][Flybus airport shuttle]] will take you from the airport to
Reykjavik and vice versa.  The bus departs right outside the airport terminal building
around 35-40 minutes after each flight arrival, and the journey to Reykjavik takes around 45
minutes.  Tickets can be bought inside the terminal building
at the Flybus booth, from the automated machine at the exit
door, or online.  Note that tickets are not sold on board the
bus itself.  Please make sure to purchase a *Flybus Plus* ticket,
which includes the additional cost for transferring to H&oacute;tel Fr&oacute;n.

---+++Practicalities

Each location mentioned on this page is shown on a
[[http://maps.google.com/maps/ms?ie=UTF8&hl=en&msa=0&msid=215425301873254406851.0004a391a0b068f8ab376&t=h&z=10][custom google map]],
and the local organisers have put together some
[[http://www.cs.nott.ac.uk/~gmh/iceland-info.pdf][general information]] for the meeting.  Tripadvisor
is useful for finding [[http://www.tripadvisor.co.uk/Restaurants-g189970-Reykjavik.html][restaurants]] and 
[[http://www.tripadvisor.co.uk/Attractions-g189970-Activities-Reykjavik.html][things to do]] in Reykjavik.

The Wednesday afternoon excursion will be a _Golden Circle_ bus tour
of some of Iceland's beautiful and dramatic natural scenery.  Please
make sure to bring sturdy footwear (e.g. walking boots), warm clothes
(e.g. waterproof jacket, fleece, hat and gloves), and a camera.

No trip to Iceland would be complete without a visit to one its
geothermal spa's, and the most famous of all is the
[[http://www.bluelagoon.com/Geothermal-spa/][Blue Lagoon]],
located 20 minutes from the airport and 40 minutes from Reykjavik.
A trip to the Blue Lagoon is highly recommended, either on route
from/to the airport, or one evening during the meeting (last entry
is 8pm).   Make sure to pack your swimming gear!

---+++Tourist information

Reykjavik is the capital city of Iceland, with a population of
around 120,000.  It is located just outside the arctic circle,
but has a temperate climate due to the gulf stream.  The weather
during the WG2.1 meeting is likely around 5C/41F.  Iceland is
famous for its unique landscape, which includes hot springs,
geysers, glaciers, lava fields, and volcanoes. 

Official tourism site for Reykjavik: http://www.visitreykjavik.is/

Official tourism site for Iceland: http://www.visiticeland.com/

Reykjavik Arts Festival (20th May to 5th June): http://www.listahatid.is/en

---+++Organisers

The meeting is organised by Luca Aceto (Reykjavik) and Graham Hutton (Nottingham).

-- Main.GrahamHutton - 20 May 2011
Topic attachments
I	Attachment	Action	Size	Date	Who	Comment
pdf	bm-slides.pdf	manage	295.5 K	05 Jul 2011 - 15:39	BernhardMoeller	Slides of Bernhard Möller's talk
pdf	jv-slides.pdf	manage	488.1 K	26 May 2011 - 23:33	JanisVoigtlaender	slides of Janis Voigtländer's talk
pdf	mss.pdf	manage	102.7 K	06 Jul 2011 - 12:28	JeremyGibbons	Slides of Jeremy Gibbons's talk at WG2.1#67