IFIP WG 2.1

Meetings

Member Pages

Members Only

Braga Portugal

IFIP21

TwoDotOneGroup, TwoDotOneObserversGroup

Minutes
Meeting information
Meeting Programme
- Schedule
Meeting organizers

Minutes

Participants

Joao Saraiva
Luis Barbosa
Hugo Macedo
Hugo Pacheco
Alcino Cunha

Organizational and administrative matters

Proxies (Fri Jan 29, 2010)

Bernhard Moller, Annie Liu -> Michel Sintzoff; Eiiti Wada -> Jeremy Gibbons.

Membership (Fri Jan 29, 2010)

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

Evaluation of conduct at meetings (Fri Jan 29, 2010)

This time the advertisements for talks didn't take very long. We will remind the participants that they can send a 1 or 2 page pdf to the secretary before the meeting, which can then be presented at the advertisements slot. The Group wants to emphasize that the use of examples to illustrate definitions helps in understanding the material presented.

Report, move Oxford pages to the wiki (Fri Jan 28, 2010)

Next meetings (Fri Jan 29, 2010)

Cohen will host Meeting #66 on the East Coast of the US, in Atlantic City. This is a seaside resort, with many casinos, about one hour from Philadelphia by bus. Ernie has contacted a boutique hotel on the boardwalk. It should be beautiful weather, and not too busy at that time of the year. Costs: about 100 euros a day + dinner costs + 5% if the number of attendants is below 22. If you have ideas or wishes about an excursion, contact Ernie. He's thinking about going to historical sites in Philadelphia.
Graham Hutton is looking into the possibility of hosting Meeting #67 in Iceland around June 2011.
In 2012 WG2.1 celebrates its 50th birthday. We will combine a one day celebration with a working group meeting. We will try to hold that meeting in February 2012 in Rome, where the 0th meeting of IFIP WG 2.1. was held.
Later meetings might be held in Australia and The Netherlands.

Formal Resolution (Fri Jan 29, 2010): The members of WG2.1 and the observers present at the 65th meeting in Póvoa de Lanhoso, Braga, Portugal, wish to thank José Nuno Oliveira, João Saraiva, Luis Barbosa and Sara Fernandes from the University of Minho for a meeting that was warm, refreshing and enlightening.
In fact, from a study of the superlative room temperatures of the meeting room and the coffee room we determined a connection that can precisely and concisely be summarized as
C |- M.
A little reflection led to glear galculations that dispelled glouds of obsgurity. After digesting what we were presented with, we ended the week at maximum density.

Technical presentations

JeremyGibbons, 50 Years of Algol 60 (Mon Jan 25, 2010, 9:30): There was a joint meeting of the BCS Advanced Programming Group and the Computer Conservation Society entitled 50 years of Advanced Programming – an Anniversary Seminar on Algol 60 in London on 14th January 2010, with presentations from, among others, Mike Woodger, Brian Wichman, and Tony Hoare (the latter delivered by Cliff Jones). There is a write-up in Issue 50 of Resurrection, the CCS Bulletin.

PatrikJansson, Parametricity and Dependent Types (Mon Jan 25, 2010, 9:57): As popularised in Wadler's "Theorems for Free" types of System F can be translated to logical relations. This translation effectively makes the types available as theorems, that you can use to reason in a higher logic framework. I will show how the idea generalizes to dependent types. In that case, the source language is powerful enough to represent logical relations, so it serves as target as well. One striking property is that we not only get theorems "for free" but their proofs as well. Joint work with Jean-Philippe Bernardy and Ross Paterson.

Zhenjiang Hu, BiG -- Bidirectional Graph Transformation (Mon Jan 25, 2010, 11:30): Bidirectional transformation is characterized by a pair of transformations, a forward transformation to produce from a source to a view, and a backward transformation to reflect modification on the view back to the source. So far, bidirectional transformation has been intensively studied in the context of relational and XML (tree) databases. It, however, remains open and challenging whether it can be addressed in the context of graphs. In this talk, I will report our recent result on bidirectional graph transformation, showing a systematic way to bidirectionalize UnCAL? , a graph algebra for the known UnQL? graph query language. The key to our bidirectionalization is full utilization of both recursive and bulk semantics of the structural recursion on graphs.

JoseOliveira, A Look at Program "G"alculation (Mon Jan 25, 2010, 15:00): The "G"alculator is a prototype of a proof assistant of a special brand, it is solely based on the algebra of Galois connections (GCs). When combined with the pointfree transform and tactics such as the indirect equality principle, GCs offer a very powerful, generic device to tackle the complexity of proofs in program verification. (The current, proof-of-concept prototype of the "G"alculator was written in Haskell by my former Ph.D. student Paulo Silva; details about the implementation can be found in our PPDP'08 paper, pages 44-55 of the proceedings.) In this presentation I would like to talk about how far we can go in exploring the "G"alculator modus operandi, not only in proofs but also in program synthesis from GCs. A relationship between this method and fold-unfold program transformation is established.(slides)

Shin-Cheng Mu, Maximum Density Segment (Mon Jan 25, 2010, 16:52): Given a list of numbers, the maximum density segment problem is to compute a segment, with length no shorter than a lower bound L, whose average (sum divided by length) is as large as possible. An amortised O(n log L) algorithm was published in 2003, and improved to O(n) next year. The problem becomes surprisingly difficult, however, if we add an upper bound for the length of feasible segments and still want an amortised linear time algorithm. Our aim was to derive/prove an algorithm using functional notations and data structures. I will talk about how our algorithm works, why adding an upper bound breaks everything, and how we tackled it.

Dave Naumann, Dynamic boundaries - information hiding interfaces for object-based programming (Tue Jan 26, 2010, 9:00): In this talk I described a way to carry out Hoare's idea to hide invariants on the internal data structures of a class-based program. Expressions denoting sets of locations, often based on ghost state, are used in the frame conditions of procedure specifications. I argued that such frame conditions can also specify a 'dynamic boundary' that reifies the intended encapsulation boundary around a module's shared mutable objects. I showed a logic that formalizes the ideas and asked for suggestions to improve the formalization.

JeremyGibbons, A calculational approach to bidirectional programming (Tue Jan 26, 2010, 11:00): Bidirectional transformation is a fundamental problem in computing—maintaining consistency of some complex source data under edits to a simpler view. There has been a lot of recent work on bidirectional programming languages, in which one obtains both forwards and backwards transformations from a single specification of the relationship between source and view. However, most of this work takes a rather syntactic approach—a domain-specific language is provided for specifying transformations and enforcing consistency, but the implementation of this language uses traditional general-purpose techniques. A more semantic approach would provide assistance to the language implementor too. We are applying for funding for a project investigating four semantic approaches to bidirectional programming—relational, higher-order, type-indexed, and parametric. We would welcome collaborators among members of the group.

Tarmo Uustalu, Explicit binds - effortless efficiency with and without trees (Tue Jan 26, 2010, 11:58): I will demonstrate a simple and robust program transformation technique that can improve asymptotic time complexity of data-manipulating programs (e.g., produce a linear-time list reversal function from the obvious quadratic one). In the version I will discuss, it applies to monadic datatypes and can be stated in two flavours, through a datatype representation, with an explicit (``frozen'') bind constructor and a special associated defining clause for the fold function, and in a functional form (generalized Church numerals), with a special definition of the bind function in terms of the build constructor. The technique explicates, systematizes, combines and scales a number of ideas known from the literature, achieving a new level of generality. Joint work with Ralph Matthes.

Larissa Meinicke, Proving atomicity using the distribution monad (Tue Jan 26, 2010, 14:58): We are currently developing a probabilistic-noninterference model for reasoning about the development of programs with security requirements. In our new model it is important to know when one can decompose a command that executes atomically. It turns out that this decomposition problem can be formulated and verified algebraically using the distribution monad. In the talk I will discuss how this might be done, and highlight a "sticking point" in the proof that we cannot currently perform algebraically. I will then ask for helpful suggestions.

Ernie Cohen, Verifying concurrent C code (Tue Jan 26, 2010, 16:46): No abstract provided.

JoseOliveira, An AoP? approach to typed linear algebra (Wed Jan 27, 2010, 9:05): In this talk I will report on first steps in the attempt to lay the (categorical) semantics of a particular class of DSLs addressing numerical programming under the motto "matrices are arrows!" This shifts the traditional view of matrices as indexed structures to typed index-free representations analogous to those of the pointfree algebra of programming (AoP? ). A parallel with binary relational algebra is established. The use of biproducts, abide-laws, fusion-laws etc in deriving linear algebra algorithms such as divide-and-conquer MMM and blocked-MMM will be emphasized. At this level, vectorization is shown to be akin to exponention if expressed in the pointfree style (vec relates to curry and unvec to uncurry). Some thoughts on how to extend the approach so as to explain algorithms such as Gaussian elimination are given. (This is on-going joint work with Hugo Macedo, Ph.D student.) (slides)

BrunoOliveira, EffectiveAdvice Disciplined Advice with Explicit Effects (Wed Jan 27, 2010, 10:08): Aspect-Oriented Programming (AOP) has been advocated by many as the "next" programming paradigm. Unfortunately, current AOP technologies have been rightfully criticized by many others for the lack of reasoning principles and unpredictably of the programs resulting from the compositions of aspects and base programs. Two key challenges on reasoning about AOP programs are 1) the ability to do modular reasoning (that is, the ability to understand a program locally without understanding the whole system) and 2) the ability to reason about interference of the different components involved in AOP composition. In this talk I will present a purely functional model of AOP-like programs that addresses the mentioned reasoning challenges using familiar reasoning techniques like equational reasoning and parametricity. Key to our work is the use of explicit effects (monads), which allow us to reason about possible effects of programs by looking only at the types of these same programs. This is join work with Tom Schrijvers and William R. Cook; a paper describing this work is available here.

AlbertoPardo, A security types preserving compiler in Haskell (Wed Jan 27, 2010, 11:45): We show the main aspects of a compiler, written in Haskell, which preserves the property of noninterference between a simple imperative language and structured machine code with loop and branch primitives. The compiler is based on the use of typed abstract syntax (represented in terms of GADTs and type families) both for the source and target language. In this case typed abstract syntax is used to model the type system for noninterference of each language where types correspond to security types. That way it is possible, on the one hand, to use Haskell's type checker to verify that programs enforce security restrictions, and on the other hand, verify that the compiler is correct (in the sense that preserves security restrictions) by construction. Joint work with Cecilia Manzino.

PatrikJansson, Testing polymorphic properties (Thu Jan 28, 2010, 9:02): This talk is about property based testing of polymorphic functions. The problem is that testing can only be performed on specific monomorphic instances, whereas parametrically polymorphic functions are expected to work for any type. We present a schema for constructing a monomorphic instance for a polymorphic property, such that correctness of that single instance implies correctness for all other instances. We also give a formal definition of the class of polymorphic properties the schema can be used for. Compared with the standard method of testing such properties, our schema leads to a significant reduction of necessary test cases. Joint work with J-P Bernardy and K Claessen - more details can be found in the associated ESOP 2010 paper

Johan Jeuring, Using Strategies for Assessment of Programming Exercises (Thu Jan 28, 2010, 9:45): At the last meeting I discussed how we want to use strategies to help students solving programming exercises. We used our approach to assess student programs in a first year functional programming course. In this talk I want to introduce how we assessed student programs using strategies, and what results we obtained from the experiment. (slides)

Doaitse Swierstra, The architecture of the Utrecht Haskell compiler (Thu Jan 28, 2010, 11:07): No abstract provided. Joint work with Atze Dijkstra, Jeroen Fokker.

Michel Sintzoff, Model refinement using bisimulations (Thu Jan 28, 2010, 11:48): A three-steps method is proposed for refining large-scale or even infinite transition systems so as to ensure correctness or efficiency. First, a given system is reduced into a smallish, finite one using a bisimulation equivalence. Second, the reduced system is refined in order to ensure a given property, using any known technique. Third, the refined reduced system is expanded back into an adequate refinement of the system given initially. This method is illustrated with a few qualitative and quantitative properties. Joint work with Roland Glueck and Bernhard Moeller.

Ernie Cohen, Infinite Atomic Actions (Thu Jan 28, 2010, 14:57): In standard sequential program semantics, useful information cannot escape a nonterminating computation. One of the charms of lazy functional programming and logic programming is that nonterminating computation can produce useful results, thanks to the imposition of an approximation ordering on the output. In Antalya, I suggested that the same trick should be possible for state-based programs, but this again required the structuring of output. However, it turns out not only that can we provide a suitable relational semantics without structuring output, but that under some reasonable assumptions, the semantics is unique.

Ernie Cohen, IImplicit and explicit flows, don't use interference (Thu Jan 28, 2010, 15:27): No abstract provided.

Doaitse Swierstra, Proxima 2.0 (Thu Jan 28, 2010, 16:18): No abstract provided. Joint work with Martijn Schrage.

Bruno Oliveira, A generic approach to binding (Fri Jan 29, 2010, 11:35): I am working on a project to investigate the application of Datatype-Generic Programming (DGP) techniques to the problem of handling variable binding on mechanized metatheory. The motivation comes from the POPLMark challenge, which asks the following question "How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs?" It turns out that existing theorem provers like Coq are already quite suitable for the task. However, one crucial issue with machine-checked formalization is that dealing with languages with binders becomes much more burdersome, because we have to prove trivial, but tedious to write, lemmas and theorems about binding otherwise not needed in hand-written proofs. Our goal is to apply DGP techniques to develop such lemmas generically, so that they can be easily reused each time for a new formalization. This talk will provide a status report of our current development.

Meeting information

Location

The 65th meeting of IFIP WG2.1 will be hosted by Jose Oliveira in Portugal, from 25 to 29 January 2010. It will take place near Braga (closest airport: Oporto). Note that POPL will be held in Madrid the week before.

Venue

The meeting will take place in the Maria da Fonte rural hotel (touristic farm) near Braga, on the way to Povoa de Lanhoso. For travelling details see the appropriate section below.

Registration and accommodation

Registration. Participants are expected to arrive on Sunday, January 24 and depart on Friday, January 29. To guarantee a room, please register by December 20, 2009. Fill in the registration form and mail it.

Payment. The registration fee will be 150€ (cash) including excursion and banquet.

Accommodation at Maria da Fonte. There are single rooms at 85,00€ per person (full board) and day. Twin rooms are at 75,00€ per person (full board) and day. For more than 20 participants, we are able to offer single rooms at 80,00€ and twin rooms at 68,00€ (per person - full board - and day). Payments will be made directly to the organization (cash or credit card).

Travelling

A shuttle service will be organized between the meeting's hotel and the airport (71kms via the A3 motorway). This will enable participants to share taxis. For this we will need the flight details of participants in advance. If you are planning to attend the meeting, please add your name to the table below as soon as possible:

Name	Arrival date	Arrival time	Arrival flight	Departure date	Departure time	Departure flight	Notes
Jose Oliveira	-	-	-	-	-	-
JeremyGibbons	24 JAN	early evening	train	29 JAN	19:35	TP0382	overnight 23/1 in Oporto
JohanJeuring	24 JAN	12:25	FR7473	29 JAN	17:30	FR7472
DoaitseSwierstra	24 JAN	12:25	FR7473	29 JAN	17:30	FR7472
Andres Loeh	24 JAN	12:25	FR7473	29 JAN	17:30	FR7472
PatrikJansson	24 JAN	15:50	LH4552	30 JAN	16:45	LH4553	leave 29/1 after lunch for Porto
Shin-Cheng Mu	24 JAN	18:55	FR5484	29 JAN	15:40	TP0734
Tarmo Uustalu	24-JAN	23h10	LH 4554	30-JAN	morning	tba
Lambert Meertens	24 JAN	12:25	FR7473	29 JAN	17:30	FR7472
Larissa Meinicke	24-JAN	10:55	LH4550	-	-	-	leave 29/1 after lunch for Porto
Peter Pepper	-	-	-	-	-	-	cancelled
Alberto Pardo	24 JAN	11:40	IB8726	29 JAN	tba	-
Zhenjiang Hu	24-JAN	21:50	TP851	29-JAN	10:20	TP426
David Naumann	24-JAN	10:10	TP1956	29-JAN	7:45	TP1953
Andy Gill	24 JAN	10:10	TP1956	29-JAN	7:45	TP1953	cancelled
Michel Sintzoff	24-JAN	12:15	SN3811	29-JAN	11:55	SN3812	(half-board.)
Bruno Oliveira	24-JAN	-	-	29-JAN	-	-
ErnieCohen	24-JAN	20:00	TAP707	29-JAN	-	SN9408	0545 airport arrival ok

Later add your flight details as soon as these become available.

Internet

Internet will be available. However, note that there is a no-computers policy during presentations (except for the presenter, and the secretary for secretarial purposes).

Latest information

(Please pay attention to this section as it will contain last minute details concerning the meeting.)

Arrival day. On the arrival day (Sunday January 24) there will be a get-together buffet dinner, which participants are welcome to join as soon as they arrive.

For the ones arriving in the morning and wishing to lunch elsewhere, please see list of restaurants around (below).

Shuttle from the airport. Please pay attention to the following schedule:

Taxi	Date	Passenger(s)	Departure
1	24-JAN	Naumann, Meinicke	As soon as Larissa arrives (10:55)
2	24-JAN	Sintzoff	12:15
3	24-JAN	Jansson	15:50
4	24-JAN	Mu (+family)	18:55
5	24-JAN	Cohen, Hu	As soon as Hu arrives (21:50)
6	24-JAN	Uustalu	23:10

Please look for somebody in the arrivals lounge holding the label "IFIP 2.1 meeting".

The fare is 70 euro per taxi (to be divided by the number of passengers). You can pay directly to the taxi driver or to the organization. Please pay directly if you need a receipt.

Shuttle to the airport. Please check the following schedule for the outgoing shuttle (Friday 29-JAN, Saturday 30-JAN):

Taxi	Date	Passenger(s)	Leaving the hotel at
1	29-JAN	Naumann, Cohen	04h45
2	29-JAN	Hu	7h30
3	29-JAN	Sintzoff	10h00
4	29-JAN	Mu (+family)	13:40
5	29-JAN	Jeuring, Swierstra, Loeh, Meertens, Gibbons	15h00, 7 seat taxi
-	29-JAN	Meinicke	going by train
-	30-JAN	Jansson	going by train
-	30-JAN	Uustalu	going by train
-	30-JAN	Pardo	staying in Braga

Meals. From Monday to Thursday, breakfast will take place at 8:00h, lunch at 12:30h and dinner at 19:30h. On Friday there will only be breakfast and lunch at the usual time.

Extras (eg. meals before buffet dinner on Sunday or later than Friday's lunch) should be paid directly to the hotel.

Payment. The organization will start collecting fees on Tuesday. Please indicate if you need a receipt. Receipts will be ready by Thursday.

You should also pay your accommodation directly to the organization (5% discount if you do this in cash).

Weather. For updated information visit your favourite weather forecast site, eg. http://www.weatheronline.co.uk/Portugal/Braga.htm

Restaurants.

Restaurant "O victor" - Tel.: +351 253 909 100; Fax: +351 253 909 101;E-mail: restaurantevictor@net.sapo.pt; WWW: www.ovictor.com; Address: Lugar do Laranjal, S.João de Rei, Povoa de Lanhoso; Opening hours: 12:30 to 15:00 / 19:30 to 22:00; GPS: 41.62.20N, 82932W.

Restaurant "Montenegro" -Tel: +351 253 631 048 / 967 870 617; Address: Calvos 4830-065 Póvoa de Lanhoso Opening hours: 12:00 to 15:00 / 19:00 to 22:00; Closed on Mondays.

Restaurant "Velho Minho" - Tel: +351 253 634 522; E-mail: hugomacedo@hotmail.com; WWW: www.velhominho.pa-net.pt; Address: Rua Dr. Manuel Ferreira, nº8 4830-542 Póvoa de Lanhoso; Opening hours: 12:15 to 15:00 / 19:25 to 23:00; Closed on Mondays.

Restaurante "Dona Melozinha" -Tel: +351 253 635 820/938 937 815; Address: Lugar de Passos - Oliveira, 4830, Póvoa de Lanhoso; Opening hours: 12h30-15h00/20h00-22h00; Closed on Sundays (evening) and Mondays.

Restaurante "Avenida" - Tel: +351 253 631 524; Address: Avenida da República - 4830-513 Póvoa de Lanhoso; Opening hours: 12:00 to 15:00 / 19:00 to 22:30; Closed on Tuesdays (evening).

Emergencies. Starting from January 24 you may use Sara Fernandes' mobile number in case of problems: +351-911-131-911 (or 911-131-911 from within Portugal)

Meeting Programme

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 default schedule is as follows:

Breakfast: 8:00
Morning sessions - 9:00 to 12:30 (coffee break at 10:30)
Lunch: 12:30
Afternoon sessions - 14:00 to 18:00 (coffee break at 16:00)
Dinner: 19:30

There will be an Welcome dinner on Monday and an excursion on Wednesday afternoon, to Guimarães (UNESCO World Heritage Site, European Capital of Culture in 2012) followed by a banquet (Wednesday evening).

Meeting organizers

-- JoseOliveira - 21.Jan.2010

Topic attachments
I	Attachment	Action	Size	Date	Who	Comment
pdf	JohanJeuringBraga.pdf	manage	436.9 K	13 May 2011 - 13:49	JohanJeuring