IFIP WG 2.1

Meetings

Member Pages

Members Only

Weltenburg Germany

IFIP21

Minutes
Latest information
Local information
Meeting Programme
- Proposed talks

Minutes

Participants

Organizational and administrative matters

Proxies (Fri 2009-04-03, 09.00): Members are reminded that proxies for voting should be reported to the chair, in writing, in advance of the meeting.

Membership (Fri 2009-04-03, 09.05): These private matters are not recorded in the public version of the minutes.

Chair (Fri 2009-04-03, 09.40): The members of IFIP WG2.1 hereby nominate Jeremy Gibbons as its new chair, to take effect prior to the sixty-fifth meeting of the group.
WG2.1 respectfully requests TC2 to consider and to endorse this nomination, and to request the cognizant officer to proceed with the matters necessary to effect the appointment of Jeremy Gibbons as chair of WG2.1.

Secretary (Fri 2009-04-03, 09.40): Johan Jeuring is to take over as WG2.1 secretary, replacing Jeremy Gibbons. This will take effect when the transfer of chair is approved by TC2.

Conduct of meeting - adverts for presentations (Fri 2009-04-03, 09.45): The advertising of talks took too long this meeting. To streamline the process, next time we will ask that participants not use laptops or other aids for their advert, and strive to be brief (so that voting can be done over morning coffee). If necessary, a single slide's worth of text—at most 12 lines, perhaps as a bitmap image—may be uploaded to the wiki or sent in advance to the secretary, and the secretary will project all such slides from the same computer.

Conduct of meeting - presentations by invited observers (Fri 2009-04-03, 09.50): Votes will still be cast and counted for presentations proposed by invited observers; however, the rank of such talks will be used only for information about topicality and not for scheduling. Instead, observers' presentations will be woven into the schedule; for example, they might be scheduled as the first couple of talks on each of Tuesday, Wednesday and Thursday mornings.

Conduct of meeting - start time (Fri 2009-04-03, 09.55): Conventionally, meetings have started at 09.30 on Monday morning, to provide a little comfort to jetlagged participants. It was felt that this was in fact of no great help; therefore, future meetings will start at 09.00 on Monday morning, the same time as all the other days during the week.

Wiki (Fri 2009-04-03, 10.00)

The wiki page http://www.cs.uu.nl/wiki/bin/view/IFIP21/ was used successfully for some of the organization of this meeting. Swierstra pointed out that he has installed a maths mode plugin that supports LaTeX formatting.

Over time, the Group will build up the content of this site:

pages from the Oxford site (such as the one about Algol) will be moved over, as time permits;
Meertens will collate information about the history of the Group;
we should grow a collection of challenge problems;
it might be nice to have a blog, with (references to) conference announcements, discussion of technical problems, arrangement of meetings and other interaction, and so on. The Group now owns the domain name http://ifipwg21.org/; this currently points to the Oxford pages, but will be changed to point to the wiki when this becomes the more useful place to start.

Book for Bob Paige (Fri 2009-04-03, 10.45): The corrected edition of Bob's book has been printed; with respect to the previous edition, it contains a new chapter by Nils Klarlund on Logic-Automata Connection and most of the pictures are in color.
Automatic Program Development: A Tribute to Robert Paige, Olivier Danvy, Fritz Henglein, Harry Mairson, Alberto Pettorossi (eds.), Springer 2008, XIV, 274 p., Hardcover, ISBN 978-1-4020-6584-2

WCDSL (Fri 2009-04-03, 10.50): The TC2 Working Conference on Domain-Specific Languages will take place at St Anne's College, Oxford on 15th to 17th July 2009. 18 papers have been accepted for presentation. A call for participation will be distributed shortly.

Meeting frequency (Fri 2009-04-03, 10.55)

We have, on the average, a meeting every 8.5 months, and lately closer to (a multiple of) 8. This means we keep cycling in the pattern Jan-Sep-May. A period of 9 months also means a cycle, like Jan-Oct-Jul-Apr.

Earlier WG meetings had no such pattern. Of the first 32 meetings, only 2 were in January; of the last 32 meetings, 8 were in January (counting #32, [ADA], in both groups).

It might be better if the meetings were spread out more, so that we do not have one quarter of the meetings in the coldest month. A uniform spread can be obtained by having a meeting every 37 weeks. Fixing target dates well in advance has several other advantages, such as making it easier to avoid clashes. Nevertheless, these dates should be just targets, with local organizers free to adapt as convenient.

Below is a list of what that would mean for the next few meetings; we believe that there are no clashes with Christmas, New Year, or Easter. (Continuing the pattern, #102 would be in the week immediately following Easter Sunday, and the scheduled week for #103, week 1 of 2037, is not a full week—it starts on a Thursday—so around then the algorithm needs some refinement.)

 Meeting #64:  week 14 of 2009: Mon 30 Mar - Fri  3 Apr 2009
 Meeting #65:  week 51 of 2009: Mon 14 Dec - Fri 18 Dec 2009
 Meeting #66:  week 36 of 2010: Mon  6 Sep - Fri 10 Sep 2010
 Meeting #67:  week 21 of 2011: Mon 23 May - Fri 27 May 2011
 Meeting #68:  week  6 of 2012: Mon  6 Feb - Fri 10 Feb 2012
 Meeting #69:  week 43 of 2012: Mon 22 Oct - Fri 26 Oct 2012
 Meeting #70:  week 28 of 2013: Mon  8 Jul - Fri 12 Jul 2013
 Meeting #71:  week 13 of 2014: Mon 24 Mar - Fri 28 Mar 2014
 Meeting #72:  week 50 of 2014: Mon  8 Dec - Fri 12 Dec 2014
 Meeting #73:  week 35 of 2015: Mon 24 Aug - Fri 28 Aug 2015
 Meeting #74:  week 20 of 2016: Mon 16 May - Fri 20 May 2016
 Meeting #75:  week  5 of 2017: Mon 30 Jan - Fri  3 Feb 2017
 Meeting #76:  week 42 of 2017: Mon 16 Oct - Fri 20 Oct 2017
 Meeting #77:  week 27 of 2018: Mon  2 Jul - Fri  6 Jul 2018
 Meeting #78:  week 12 of 2019: Mon 18 Mar - Fri 22 Mar 2019
 Meeting #79:  week 49 of 2019: Mon  2 Dec - Fri  6 Dec 2019
 Meeting #80:  week 34 of 2020: Mon 17 Aug - Fri 21 Aug 2020
 Meeting #81:  week 19 of 2021: Mon 10 May - Fri 14 May 2021
 Meeting #82:  week  4 of 2022: Mon 24 Jan - Fri 28 Jan 2022
 Meeting #83:  week 41 of 2022: Mon 10 Oct - Fri 14 Oct 2022
 Meeting #84:  week 26 of 2023: Mon 26 Jun - Fri 30 Jun 2023
 Meeting #85:  week 11 of 2024: Mon 11 Mar - Fri 15 Mar 2024
 Meeting #86:  week 48 of 2024: Mon 25 Nov - Fri 29 Nov 2024
 Meeting #87:  week 33 of 2025: Mon 11 Aug - Fri 15 Aug 2025
 Meeting #88:  week 18 of 2026: Mon 27 Apr - Fri  1 May 2026
 Meeting #89:  week  3 of 2027: Mon 18 Jan - Fri 22 Jan 2027
 Meeting #90:  week 40 of 2027: Mon  4 Oct - Fri  8 Oct 2027
 Meeting #91:  week 25 of 2028: Mon 19 Jun - Fri 23 Jun 2028
 Meeting #92:  week 10 of 2029: Mon  5 Mar - Fri  9 Mar 2029
 Meeting #93:  week 47 of 2029: Mon 19 Nov - Fri 23 Nov 2029
 Meeting #94:  week 32 of 2030: Mon  5 Aug - Fri  9 Aug 2030
 Meeting #95:  week 17 of 2031: Mon 21 Apr - Fri 25 Apr 2031
 Meeting #96:  week  2 of 2032: Mon  5 Jan - Fri  9 Jan 2032
 Meeting #97:  week 39 of 2032: Mon 20 Sep - Fri 24 Sep 2032
 Meeting #98:  week 24 of 2033: Mon 13 Jun - Fri 17 Jun 2033
 Meeting #99:  week  9 of 2034: Mon 27 Feb - Fri  3 Mar 2034
 Meeting #100: week 46 of 2034: Mon 13 Nov - Fri 17 Nov 2034

Next meetings (Fri 2009-04-03, 11.10)

Meeting #65 will be hosted near Braga in Portugal by José Oliveira, probably in January 2010 (because the new target week of 14th December is deemed to be too close to Christmas). Oliveira will shortly send round a selection of possible venues and weeks for comment.
Cohen has volunteered to host Meeting #66 on the East Coast of the US, perhaps in Philadelphia or Atlantic City.
Hutton is exploring the possibility of hosting Meeting #67 in Iceland.

Formal Resolution (Fri 2009-04-03, 11.15): The members of WG2.1 and the observers present at the 2⁶th meeting in Weltenburg Abbey, Germany wish to thank Bernhard Möller and his assistants from the University of Augsburg, for arranging a splendid meeting in convivial surroundings.
Our exertions during the week brought us to a high level, from which we had a broad overview; we subsequently experienced a breakthrough involving a stream. Even if we were in the dark when we arrived, we were transported into enlightenment, where happily we learned that the abstract notion of clouds has a firm concrete implementation in terms of beer kegs.

Technical presentations

Note: presentation summaries were prepared by the speakers.

CarrollMorgan, The Tale of the Three Judges (Mon 2009-03-30, 11.30)

Three judge-bots communicate over the internet to publish jointly a majority decision of guilt or innocence; but neither an observer nor any of the 'bots is to be able to deduce from that overall judgement what any of the individual judgements might have been. How is this done? A proper explication "in our style" would be a derivation of a protocol that was correct by construction; but that is rare in the security world.

Rare or not, I'll use this example to present a layered development of the protocol where (as we expect) each layer's correctness is evident from the specifications of the components it uses, and they in turn refer to lower layers still. Specifically, the overall Three Judges' Protocol uses two instances of Yao's Two-Party propositional scheme then one instance of Rivest's Oblivious Transfer; the propositional schemes themselves use Oblivious Transfer again; and all of those rely ultimately on the Encryption Lemma.

All the reasoning is program-algebraic (well, almost all of it); and although the calculations are pretty pedestrian at least it is algebra. The important thing is that the notion of security is compositional (and in more interesting cases monotonic with respect to refinement), and getting that model right was a real eye-opener. The model is of course crucial to determining the algebra.

GrahamHutton, The Worker/Wrapper Transformation (Mon 2009-03-30, 13.50): The worker/wrapper transformation is a technique for changing the type of a computation, usually with the aim of improving its performance. It has been used by compiler writers for many years, but the technique is little known in the wider functional programming community, and has never been described precisely. In this talk we explain, formalise and explore the generality of the worker/wrapper transformation. We also provide a systematic recipe for its use as an equational reasoning technique for improving the performance of programs, and illustrate the power of this recipe using a range of examples. (Based upon joint work with Andy Gill, from a recent paper in JFP.)

RalfHinze, Trees (Mon 2009-03-30, 14.35): No abstract provided.

BrunoOliveira, The Different Aspects of Monads and Mixins (Mon 2009-03-30, 16.10)

Around twenty years ago two important developments happened in the areas of modularity and reuse in programming languages. On the one hand, Moggi showed how computational effects found in impure languages could be simulated using the notion of monads from category theory. Inspired by Moggi's work, Wadler showed how monads could be used to structure (purely functional) programs. On the other hand, work by Cook showed how variations of mixins could model different notions of inheritance (normally found in object-oriented languages) in simple, elegant and compositional ways, by using traditional techniques of fixed-point theory.

Monads and mixins are helpful to handle different aspects of modularity and reuse in programming languages, yet they have been largely explored independently. In this talk I will show that the combination of monads and mixins leads to a simple aspect-oriented programming style that can be used effectively in purely functional programming languages to write elegant, reusable and modular programs.

A draft paper is available here.

JulesDesharnais, MPC and AMAST 2010 (Mon 2009-03-30, 17.15): No abstract provided.

EricHehner, A Probability Perspective (Tue 2009-03-31, 09.00): I draw together four perspectives that contribute to a new understanding of probability and solving problems involving probability. The first is the Subjective Bayesian perspective that probability is affected by one's knowledge, and that it is updated as one's knowledge changes. The problem of assigning prior probabilities is mitigated by the Information Theory perspective, which equates probability with information. The main point is that the formal perspective (formalize, calculate, unformalize) is beneficial to solving probability problems. And finally, the programmer's perspective provides us with a suitable formalism. A paper can be found at http://www.cs.utoronto.ca/~hehner/ProPer.pdf.

JohanJeuring, Constructing Strategies for Programming (Tue 2009-03-31, 11.05): Learning to program is difficult. To support learning programming, we want to develop an intelligent tutoring systems for learning programming. In this talk we illustrate how to construct strategies for solving programming exercises and how these strategies can be used to automatically support students using an intelligent programming tutor to incrementally develop a program.

ConorMcBride, Ornamental Algebras, Algebraic Ornaments (Tue 2009-03-31, 11.50): Lists can be seen as an annotated version of natural numbers, labelling each "successor" symbol with an element. The dependent family of vectors can be seen as a refinement of lists, indexing by length. In this talk, I structure the coding of types by data so as to express these refinements and annotations, presenting new datatypes as "ornamented" versions of old. Every ornament induces an algebra whose fold takes the fancy new type to the plain old type by rubbing out the added information. Meanwhile, every algebra induces an ornament which indexes by its carrier. With these two facts, I shall attempt to abolish some previously astonishing coincidences. The longer-term prospect is that we may be able to manage the diversity and complexity of dependent datatypes with algebraic instruments previously found only in the construction of programs.

DiethardMichaelis, Boolean Algebras Have an Embarrassingly Rich Structure (P.R. Halmos, 1956) (Tue 2009-03-31, 14.35): Most of this structure is not only mathematically appealing but also (predicate) calculationally useful. Beyond the traditionally well known lattice structure we have Boolean groups, Boolean vectorspaces, Boolean rings and the everywhere operator. There is a pointfree theory of the Boolean quantifiers which elegantly and compactly covers much of ordinary Boolean quantifier theory (including a pointfree characterisation of the ugly "does not occur in" proviso). Punctual "predicate transformers" (Boolean algebra endofunctions) give an algebraic view on "Boolean expressions".
Occasional notational considerations will be unavoidable. There will be some application, calculational proof, and derivation, too. And there is more: relativization, Boolean homomorphism, partial order and implication, ..., from which most has to be left untold in order to stay within my time limit.

DoaitseSwierstra, Attribute Grammars Fly First Class (Tue 2009-03-31, 16.05): No abstract provided.

RolandBackhouse, Richard Bird's Fan Club (Wed 2009-04-01, 09.00)

A year ago, Richard Bird sent me the following problem, which he was unable to solve.

Consider a natural transformation tr :: L -> FL. Suppose tr has the property that it returns an F-structure of L-structures all of the same shape. Consider the instance trG :: LG -> FLG. I want to show that if trG is applied to an L-structure of G-structures all of the same shape, then it returns a result that is an F-structure of LG-structures all of the same shape.

The generic theory of "fan"s and "zip"s pioneered by Backhouse, Doornbos and Hoogendijk in 1992, and which eventually formed Hoogendijk's 1997 PhD thesis, is the appropriate vehicle for tackling such problems. A "fan" of F is a relation between values and F-structures of arbitrary shape.

In this talk, we introduce a collection of fans inspired by Richard's problem (hence "Richard Bird's fan club") and we explore the relation between them. Time permitting, we will introduce the algebraic structure of shape properties of datatypes.

The talk will begin with a short introduction for the benefit of non-"fan"atics.

(The talk is based on a draft paper by myself, Richard and Paul Hoogendijk. A consequence of the joint authorship is that the title has had to change, but I think the older title is nicer! See http://www.cs.nott.ac.uk/~rcb/papers/abstract.html#FanClub for further details and the paper.)

LambertMeertens, Semantic Typing of Indeterminate Terms (Wed 2009-04-01, 10.45)

When indeterminacy is allowed in specifications, a term may possibly be refined to several different and not interconvertible terms. For example, the term "~S" in Hehner's bunch calculus stands for an indeterminate choice from set S and may be refined to any element of S. The denotational meaning of a ground term is then the collection of values to which it may be refined. Thus, while the "syntactic" type of term ~{0} is Nat (assuming that 0 has type Nat), since ~{0} = 0, its "semantic" type is Set(Nat).

Many years ago, when discussions about hot and cold indeterminacy were a staple of WG2.1 meetings, I tried to define the semantic typing of a simple calculus of indeterminate terms, but could not get it to work: syntactically well-typed terms were not always properly typed semantically. From time to time I revisited this, in the conviction that this could not be hard, but each time there was some glitch. I even tried to enumerate all possible reasonable typing methods, but all broke down somewhere. Then I lost interest and gave up.

A few weeks ago I woke up in the middle of the night with the idea that I had the solution, which was "obviously correct". I jotted it down -- just three lines -- and went back to sleep. The next morning I found the "note to self", which (unlike some other notes produced in a likewise manner) was not gibberish but made sense. Rather skeptical after my previous experiences, I started the verification, and, to my amazement, succeeded. The presentation consists of that verification. While relatively straightforward, it is not trivial.

JoseOliveira, Towards "Middle School" MPC (Wed 2009-04-01, 11.40): Why is the mathematics of program construction (MPC) a privilege of higher education? What prevents us from teaching (say) 12-year students how to derive simple (eg. functional) algorithms from their maths textbooks? Wouldn't this even contribute to stimulating maths teaching itself? In the MathIS? project at Minho we are planning a series of experiments with middle-school maths teachers which go in this direction. In this talk I will present some little experiments of mine, some of which already tried out with (programming illiterate) students doing an arts degree. These experiments, to be presented in increasing order of complexity, include the use of mutual recursion to calculate “for-loops” from maths expressions involving quantifiers (eg. summations, etc).

JeremyGibbons, Unfolding Data Abstractions (Thu 2009-04-02, 09.00): Data abstractions—with public interfaces hiding private implementations—represent a form of codata rather than ordinary data, and so proof methods for corecursive programs are the appropriate techniques to use for reasoning with them. In particular, we show that the universal properties of unfold operators are perfectly suited for the task.

AndresLoeh, Generic Diff (Thu 2009-04-02, 10.40): No abstract provided.

EiitiWada, The Art of Happy Hacking Calculator Programming (Thu 2009-04-02, 11.55)

Happy Hacking Calculator

for iPod touch
stack machine
reverse polish notation

Instructions

 + (b a ...) → (a+b ...)
 - (b a ...) → (a-b ...)
 * (b a ...) → (a*b ...)
 / (b a ...) → (q r ...)  where q=a div b, r=a mod b
 H,D,O change radix
 E(enter) separate 2 numerals
 ^ (b a ...) → (a ...)  pop
 " (a ...) → (a a ...)  duplicate
 : (b a ...) → (a b ...)  exchange
 _ (a ...) → (-a ...)  negate
 S(square root) (a ...) → (q r ...)  where a=q*q+r
 F(factorize) (a ...) → (p k r ...)  where a=p^k*r
 P(power) (b a ...) → (a^b ...)
 J(julian date) (yyyymmdd ...) → (Julian date of yyyy mm dd ...)

secondary stack

 U(up) (...) (a ...) → (... a) (...)
 N(down) (... a) (...) → (...) (a ...)
 = define program
 G negative jump

program examples:

rotation
```
 (:U:U:NN)R=
 
```

trace

 (...)(4 3 2 1 ...)
 : (...)(3 4 2 1 ...)
 U (... 3)(4 2 1 ...)
 : (... 3)(2 4 1 ...)
 U (... 3 2)(4 1 ...)
 : (... 3 2)(1 4 ...)
 N (... 3)(2 1 4 ...)
 N (...)(3 2 1 4 ...)

sum of 1,2,...,10
```
 (0Ua"N+U1-"_aG^N)X=
 
```

trace

 0 (...)(0 ...)
 U (... 0)(...)
 a (... 0)(10 ...)
 " (... 0)(10 10 ...)   (... 10)(9 9 ...)        (... 54)(1 1 ...)
 N (...)(0 10 10 ...)   (...)(10 9 9 ...)        (...)(54 1 1 ...)
 + (...)(10 10 ...)     (...)(19 9 ...)          (...)(55 1 ...)
 U (... 10)(10 ...)     (... 19)(9 ...)          (... 55)(1 ...)
 1 (... 10)(1 10 ...)   (... 19)(1 9 ...)        (... 55)(1 1 ...)
 - (... 10)(9 ...)      (... 19)(8 ...)          (... 55)(0 ...)
 " (... 10)(9 9 ...)    (... 19)(8 8 ...)        (... 55)(0 0 ...)
 _ (... 10)(-9 9 ...)   (... 19)(-8 8 ...)       (... 55)(0 0 ...)
 a (... 10)(10 -9 9 ...)(... 19)(10 -8 8 ...)    (... 55)(10 0 0 ...)
 G (... 10)(9 ...)      (... 19)(8 ...)          (... 55)(0 ...)
 ^                                               (... 55)(...)
 N                                               (...)(55 ...)

factorial
```
 ("_6_G1+5_"G"1-!*)!=
 
```

trace

 ! (3)
 " (3 3)      (2 2 3)     (1 1 2 3)     (0 0 1 2 3)
 _ (-3 3)     (-2 2 3)    (-1 1 2 3)    (0 0 1 2 3)
 7 (7 -3 3)   (7 -2 2 3)  (7 -1 1 2 3)  (7 0 0 1 2 3)
 _ (-7 -3 3)  (-7 -2 2 3) (-7 -1 1 2 3) (-7 0 0 1 2 3)
 G (3)        (2 3)       (1 2 3)       (0 1 2 3)
 0 ^                                      (1 2 3)
 -1 1                                      (1 1 2 3)
 -2 E                                      (1 1 2 3)
 -3 5                                      (5 1 1 2 3)
 -4 _                                      (-5 1 1 2 3)
 -5 "                                      (-5 -5 1 1 2 3)
 -6 G                                      (1 1 2 3)
 -7 " (3 3)      (2 2 3)     (1 1 2 3)
 -1 1 (1 3 3)    (1 2 2 3)   (1 1 1 2 3)
 -2 - (2 3)      (1 2 3)     (0 1 2 3)
 -3 ! (2 3)      (1 2 3)     (0 1 2 3)
 -4 * (6)          (2 3)       (1 2 3)
 -5

Ackermann function Sussman SICP ex1.10

 (define (A x y)
 (cond ((= y 0) 0)
 ((= x 0) (* 2 y))
 ((= y 1) 2)
 (else (A (- x 1) (A x (- y 1))))))
 
 ("1-45_G:"1-30_G:"2-f_GU"1-:N1-AA18_"G^^2Ea_"G^2*3_"G^^0)A=
 111111111122222222223333333333444444
 y=0->0  0123456789012345678901234567890123456789012345
 111111111122222222223
 x=0->(* 2 y)    0123456789012345678901234567890      0123
 111111                 1
 y=1->2                 0123456789012345       01234567890
 111111111
 else(A (- x 1) (A x (- y 1)))         0123456789012345678
 (y x)
 U (y) (x)            xEyA
 " (y) (x x)          1E10A=>1024
 (y) (x-1 x)
 : (y) (x x-1)
 N (y x x-1)
 (y-1 x x-1)
 A (A(x y-1) x-1)
 A (A(x y)

Date of Easter (Knuth TAOCP 1.3.2'-32)

 G←(Y mod 19)+1
 C←floor(Y/100)+1
 X←floor(3C/4)-12
 Z←floor((8C+5)/25)-5
 D←floor(5Y/4)-X-10
 E←(11G+20+Z-X)mod 30
 if(E=25&&G>11||E=24)E←E+1
 N←44-E
 if(N<21)N←N+30
 N←N+7-((D+N)mod 7)
 if(N>31)(N-31)April else N March

Future works:

to implement into iPod touch
to work for the art of programming without variables
to write the assembly program or compiler
to consider the orders in stack for optimal computation
to gather a lot of usable programs or examples
etc. etc.

KeesKoster? , Text Mining for Intellectual Property (Thu 2009-04-02, 14.00)

For many professional search applications, the effectiveness of traditional word-based search engines is not adequate. That is why biomedical search and patent search, somewhat outside the main stream of Information Retrieval, have been pioneers in Text Mining, characterized by: search using linguistic phrases instead of keywords; use of thesauri and named entity recognition; aggregation and structured presentation of the search results.

In this talk, I first describe the rationale behind the prototype search engine PHASAR, which uses dependency triples instead of words to represent both the documents and the queries. Then I will demonstrate its use in an experimental literature mining system for the Biosciences, which gives access to over 17 million Medline abstracts.

Finally, I describe the TM4IP project, in which a text mining system based on PHASAR and suitable for patent mining is to be developed. Patent texts are notoriously complicated technical texts, providing major challenges for both parsing and search technology. I describe these challenges, and the solutions (using parsing and indexing techniques inspired by a long experience in compiler construction) that are needed in order to build a truly useful patent mining system.

Varmo Vene, Corecursive Algebras (Thu 2009-04-02, 16.05): We study general structured corecursion, dualizing the work of Osius, Taylor, and others on general structured recursion. We call an algebra of a functor corecursive if it supports general structured corecursion: there is a unique map to it from any coalgebra of the same functor. The concept of antifounded algebra is a statement of the bisimulation principle. We show that it is independent from corecursiveness: Neither condition implies the other. Finally, we call an algebra focusing if its codomain can be reconstructed by iterating structural refinement. This is the strongest condition and implies all the others.

Thomas Weigert, Lessons Learned from Deploying Program Transformations to Implement Large-Scale Industrial Systems (Thu 2009-04-02, 16.45): For a number of years, we have used a program-transformation environment to realize UML and SDL designs of large industrial systems through high-performance implementations. In this talk, I want to high-light some of the lessons we had to learn about what worked and what did not work (at least, for us) when attempting to deploy such environment in an industrial environment with real users, developing large, embedded systems. While these are not great pearls of wisdom, nevertheless, we ran afoul of many of these insights, and had to suffer with frustrated users and time-consuming reimplementations.
Background: Inspired by a collaboration with Jim Boyle I had implemented a program transformation system in the early nineties. This system grew over the years into an environment for developing industrial-strength applications consisting of: (i) verification of scenario-based specification by ensuring these are consistent and complete via a hybrid theorem-prover/model checker; (ii) generation of test suites from the scenario specifications; (iii) synthesis of UML designs from the scenario specifications; (iv) weaving of multiple design fragments into a single large design; (v) transformation of these designs into highly optimized C code; and (vi) executing the test suites against that code.

JoseOliveira, Calculating with Pointfree Alloy (Fri 2009-04-03, 11.50): Alloy is known as a lightweight formal method based on a declarative modeling language whose syntax has an object-oriented flavour, if not UML-like. What is perhaps less known is that Alloy's logic draws much from the relational formalisms of Tarski-Givant's "set theory without variables", as the aphorism "in Alloy, everything is a relation" tells. The language even includes a pointfree (PF) subset which promotes "relational thinking" in a natural way. In this talk I will show how to use the PF-transform to convert pointwise Alloy into pointfree so as to discharge proof obligations by algebraic calculation in AOP (algebra of programming) style. The approach includes the use of (allegorial) diagrams whose commuting squares depict not only data models but also facts about them (vulg. invariants). They also serve to guide the calculation of weakest preconditions for the operations to be properly type-checked in an Alloy model. This paves the way to the sketch of a little repository of generic invariants capturing ubiquitous requirements in MDE such as referential integrity, functional dependencies, closures, etc. An illustration of the approach will be given taken from the VFS (Verified File System) case study, the challenge put forward by Rajeev Joshi and Gerard Holzmann in 2007.

Latest information

1. Arrival
Please notify us when and where you will arrive by train. We will have a small shuttle bus available and can pick you up in reasonable groups. If you cannot make it till 20:00 on Sunday March 29, don't worry, we'll have the key to the monastery to let you in.

2. Money
You'll need to bring the registration fee (EUR 150) plus accommodation (normally 5 nights at EUR 55 each) plus money for drinks etc., all in cash.
That's a total amount of EUR 425.

3. Weather
At the time of the meeting weather is fairly unpredictable, so best bring winter, rain and spring clothing and, most important, good shoes. At the moment the forecast is rainy and a temperature around 5 degrees Celsius.

4. Excursion
We plan to have a walking tour in the surroundings of the monastery, ended by a boat trip through the gorges of the Danube back to the monastery. In case of catastrophic weather we may instead go to Regensburg to do some sightseeing.

5. Emergencies
Starting from March 27 you may use the Peter Höfner's mobile number in case of problems: +49-176-61244060 (or 0176-61244060 from within Germany)

Local information

Location

The 64th meeting of IFIP WG2.1 will be held at Weltenburg Abbey, Bavaria, Germany (see also Wikipedia page), from 30th March to 3rd April 2009, hosted by Bernhard Möller.

The organizers have put up some local information; note that bookings have to be completed by 15th January 2009.

Internet

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

Schedule

We will start at 9:30 on Monday, 9:00 the following days, and finish around noon on Friday. Please arrange to be there for the whole meeting.

There will be an excursion (probably Wednesday afternoon), and a banquet (probably Thursday evening). The first half of Friday morning is taken up with a Members-Only Meeting; observers may have a leisurely breakfast.

Meeting Programme

Proposed talks

The following talks have been proposed and will be ready for presentation at the start of the meeting. The first few talks may be selected from this list.

DoaitseSwierstra, Typed Transformation of Typed Abstract Syntax (1 hour): Advantages of embedded domain-specific languages (EDSLs) are that one does not have to implement a separate type system nor an abstraction mechanism, since these are directly borrowed from the host language. Straightforward implementations of embedded domain-specific languages map the semantics of the embedded language onto a function in the host language. The semantic mappings are usually compositional, i.e. they directly follow the syntax of the embedded language.
One of the questions which arises is whether conventional compilation techniques, such as global analysis and resulting transformations, can be applied in the context of EDSLs. The approach we take is that, instead of mapping the embedded language directly onto a function, we first build a representation of the abstract syntax tree of the embedded program fragment. This syntax tree is subsequently analyzed and transformed, and finally mapped onto a function representing its denotational semantics. In this way we achieve run-time ``compilation'' of the embedded language. Run-time transformations on the embedded language can have a huge effect on performance. In previous work (Haskell Symposium 2008) we presented a case study comparing the |Read| instances generated by Haskells |deriving| construct with instances on which run-time grammar transformations (precedence resolution, left-factorisation and left-corner transformation) have been applied. In this paper we present the library, which has an arrow like interface, which supports in the construction of analyses and transformations, and we demonstrate its use in implementing a common sub-expression elemination transformation. The library uses typed abstract syntax to represent fragments of embedded programs containing variables and binding structures, while preserving the idea that the type system of the host language is used to emulate the type system of the embedded language. The tricky issue is how to keep a collection of mutually recursive structures well-typed while it is being transformed. We finally discuss the typing rules of Haskell, its extensions and those as implemented by the GHC and show that pure System-F based systems are sufficiently rich to express what we want to express, albeit at the cost of an increased complexity of the code.

JeremyGibbons, CancerGrid: Model- and Metadata-Driven Clinical Trials Informatics: The CancerGrid project (http://www.cancergrid.org/) is developing a software architecture for so-called "tissue-plus-data" clinical trials. The project is using a model- and metadata-driven approach that makes the semantics of clinical trials explicit; the trial protocol, required anyway for regulatory purposes, is a sufficient model from which to generate software support, and suitable metadata annotations facilitate dataset discovery and reuse. We believe that the approach has wide applicability, to any data-rich distributed community - not just medical informatics, but also for example electronic government. Since it involves transformations (of trial models into services), it might be of interest to group members.

EricHehner, A Probability Perspective: I draw together four perspectives that contribute to a new understanding of probability and solving problems involving probability. The first is the Subjective Bayesian perspective that probability is affected by one's knowledge, and that it is updated as one's knowledge changes. The problem of assigning prior probabilities is mitigated by the Information Theory perspective, which equates probability with information. The main point is that the formal perspective (formalize, calculate, unformalize) is beneficial to solving probability problems. And finally, the programmer's perspective provides us with a suitable formalism. A paper can be found at http://www.cs.utoronto.ca/~hehner/ProPer.pdf.

CarrollMorgan, The Tale of the Three Judges (45-60 mins)

DiethardMichaelis, Boolean algebras have an embarrassingly rich structure (P.R. Halmos, 1956). (approx. 1h): Most of this structure is not only mathematically appealing but also (predicate) calculationally useful. Beyond the traditionally well known lattice structure we have Boolean groups, Boolean vectorspaces, Boolean rings and the everywhere operator. There is a pointfree theory of the Boolean quantifiers which elegantly and compactly covers much of ordinary Boolean quantifier theory (including a pointfree characterisation of the ugly "does not occur in" proviso). Punctual "predicate transformers" (Boolean algebra endofunctions) give an algebraic view on "Boolean expressions".
Occasional notational considerations will be unavoidable. There will be some application, calculational proof, and derivation, too. And there is more: relativization, Boolean homomorphism, partial order and implication, ..., from which most has to be left untold in order to stay within my time limit.

RolandBackhouse, Richard Bird's Fan Club (45 mins)

A year ago, Richard Bird sent me the following problem, which he was unable to solve.

Consider a natural transformation $tr :: L \to FL$ . Suppose has the property that it returns an -structure of -structures all of the same shape. Consider the instance $trG :: LG \to FLG$ . I want to show that if is applied to an -structure of -structures all of the same shape, then it returns a result that is an -structure of -structures all of the same shape.

is a relation between values and

-structures of arbitrary shape.

The talk will begin with a short introduction for the benefit of non-"fan"atics.

RolandBackhouse, A Penny Game (30 mins): Penney Ante is a probabilistic game played with pennies and invented by Walter Penney. John Horton Conway has formulated a very concise and easy-to-use formula for optimising one's odds of winning. However, typical proofs of the formula are complicated by the use of probabilistic generating functions. We give a (relatively) simple derivation of Conway's formula.
Subsequent literature tackles a more general problem but appears to be flawed. If time permits, this more general problem will be reviewed.

JeremyGibbons, Unfolding Abstract Datatypes: Abstract datatypes — with public interfaces hiding private implementations — represent a form of codata rather than ordinary data, and so proof methods for corecursive programs are the appropriate techniques to use for reasoning with them. In particular, we show that the universal properties of unfold operators are perfectly suited for the task. We illustrate with the solution to a problem in the recent literature.

ConorMcBride, Ornamental Algebras, Algebraic Ornaments (60min): Lists can be seen as an annotated version of natural numbers, labelling each "successor" symbol with an element. The dependent family of vectors can be seen as a refinement of lists, indexing by length. In this talk, I structure the coding of types by data so as to express these refinements and annotations, presenting new datatypes as "ornamented" versions of old. Every ornament induces an algebra whose fold takes the fancy new type to the plain old type by rubbing out the added information. Meanwhile, every algebra induces an ornament which indexes by its carrier. With these two facts, I shall attempt to abolish some previously astonishing coincidences. The longer-term prospect is that we may be able to manage the diversity and complexity of dependent datatypes with algebraic instruments previously found only in the construction of programs.

EiitiWada, Programmable Calculator for iPod touch (30min)

Stack based calculator was designed and implemented. Enhanced version is now running on the simulator, which has secondary stack, program storage and evaluator.

3*(2+1) is entered like

3E2E1+* -> 9            ;`E' separates 2 numerals

factorial is defined by

("_7_G^1E5_"G"1-!*)!=

3! -> 6
5! -> 120

Other examples, tested on the simulator, will also be shown.

Ackermann function (Sussman, SICP exercise 1.10)

("1-46_G:"1-31_G:"2-15_GU"1-:N1-AA20_"G^^2Ea_"G^2*3_"G^^0)A=
1E10A -> 1024
3E3A -> 65536

Date of Easter (Knuth, TAOCP exercise 1.3.2'-32)

("U"100/1+:^"3*4/12-"N5*4/:^:-10-U:^U)A=
(8*5+25/5-U^19/^1+"11*20+N+N-30/^:U)B=
("24-27_G"_25+18_G"25-9_GN"U12-2_G1+N^)C=
(44:-"_21+3_G30+"U7+NN+7/^-"32-3_G69+300+)K=
2009ABCK -> 412         ;april 12

g function for Meertens' number (Bird, Introduction to FP)

(1+""F:^:^:-dG)x=       ;next prime number
(10E)B=                 ;radix=10
(1:1U0U"N1+"UB:P-5_G1_18G)g=
(N1-"U"26_GB:P/NN:Ux"N:UU:PU:N*:1_36GNN^^^^)h=
402g -> 400
430g -> 432
81312000gh -> 81312000

Spigot algorithm for Pi (Pi=g(1,0,1,1,3,3))
```
3E3E1E1E0E1g -> Pi
```

JoseOliveira, Calculating with Pointfree Alloy (approx. 45m): Alloy is known as a lightweight formal method based on a declarative modeling language whose syntax has an object-oriented flavour, if not UML-like. What is perhaps less known is that Alloy's logic draws much from the relational formalisms of Tarski-Givant's "set theory without variables", as the aphorism "in Alloy, everything is a relation" tells. The language even includes a pointfree (PF) subset which promotes "relational thinking" in a natural way. In this talk I will show how to use the PF-transform to convert pointwise Alloy into pointfree so as to discharge proof obligations by algebraic calculation in AOP (algebra of programming) style. The approach includes the use of (allegorial) diagrams whose commuting squares depict not only data models but also facts about them (vulg. invariants). They also serve to guide the calculation of weakest preconditions for the operations to be properly type-checked in an Alloy model. This paves the way to the sketch of a little repository of generic invariants capturing ubiquitous requirements in MDE such as referential integrity, functional dependencies, closures, etc. An illustration of the approach will be given taken from the VFS (Verified File System) case study, the challenge put forward by Rajeev Joshi and Gerard Holzmann in 2007. (slides)

JoseOliveira, Matrices are Arrows! an AOP perspective on (typed) linear algebra (approx. 30m): The advent of on-chip parallelism poses many challenges to current programming languages. Traditional approaches based on compiler or hand-coded optimizations are giving place to trendy generative techniques, based on DSLs for high-level program transformation. 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 an index-free representation analogous to that of the pointfree algebra of programming (AOP). The use of biproducts, abide-laws, fusion-laws etc to reason about particular matrix transforms such as those used in Gaussian elimination, LU decomposition and so on will be emphasised . (This is on-going joint work with Hugo Macedo, Ph.D student.)

JoseOliveira, Towards "middle school MPC" (approx. 30m): Why is the mathematics of program construction (MPC) a privilege of higher education? What prevents us from teaching (say) 12-year students how to derive simple (eg. functional) algorithms from their maths textbooks? Wouldn't this even contribute to stimulating maths teaching itself? In the MathIS? project at Minho we are planning a series of experiments with middle-school maths teachers which go in this direction. In this talk I will present some little experiments of mine, some of which already tried out with (programming illiterate) students doing an arts degree. These experiments, to be presented in increasing order of complexity, include the use of mutual recursion to calculate “for-loops” from maths expressions involving quantifiers, eg. summations, etc. (slides)

AlbertoPardo, An extended form of shortcut fusion with multiple applications (approx. 45min): Functional programs often combine separate parts using intermediate data structures for communicating results. These programs are modular, easier to understand and maintain, but suffer from inefficiencies due to the generation of those gluing data structures. To eliminate such redundant data structures, some program transformation techniques have been proposed. One such technique is shortcut fusion. In this talk, we will present an extended form of shortcut fusion such that, in addition to intermediate structures, the program parts may now communicate context information or even effects, and it is still possible to eliminate those structures. We show that this extension can be used in multiple cases, such as, the elimination of intermediate structures in compositions of monadic programs, the derivation of both purely-functional and monadic circular programs, and the derivation of both purely-functional and monadic higher-order programs. (This is a joint work with João Paulo Fernandes and João Saraiva)

BrunoOliveira, The Different Aspects of Monads and Mixins (approx. 45min)

A draft paper is available here.

GrahamHutton, The worker/wrapper transformation: The worker/wrapper transformation is a technique for changing the type of a computation, usually with the aim of improving its performance. It has been used by compiler writers for many years, but the technique is little known in the wider functional programming community, and has never been described precisely. In this talk we explain, formalise and explore the generality of the worker/wrapper transformation. We also provide a systematic recipe for its use as an equational reasoning technique for improving the performance of programs, and illustrate the power of this recipe using a range of examples. (Based upon joint work with Andy Gill, from a recent paper in JFP.)

Kees Koster, Text Mining and Data Mining

Finally, I describe the TM4IP project, in which a text mining system based on PHASAR and suitable for patent mining is to be developed. Patent texts are notoriously complicated technical texts,providing major challenges for both parsing and search technology. I describe these challenges, and the solutions (using parsing and indexing techniques inspired by a long experience in compiler construction) that are needed in order to build a truly useful patent mining system.

PeterHoefner, Automated Reasoning in Variants of Kleene Algebras

It has often been claimed that model checking, special purpose automated deduction or interactive theorem proving are needed for formal program development. We demonstrate that off-the-shelf automated proof and counterexample search is an interesting alternative if combined with the right domain model. As a result we show that variants of Kleene and relation algebras might provide formal methods with high potential for automation.

The first part of the talk will focus on case studies where this approach was successfully applied, including Hoare logic and refinement calculus. The second part outlines how this can be extended to an algebraic verification environment for programs and software systems. Since there is a lot more to do, we point out some further directions.

(joint work with H.-H. Dang, B.Möller, G. Struth and others)

PeterHoefner, An Algebra of Product Families: Experience from recent years has shown that it is often advantageous not to build a single product but rather a family of similar products that share at least one common functionality while having well-identified variabilities. Such product families are built from elementary features that reach from hardware parts to software artefacts such as requirements, architectural elements or patterns, components, middleware, or code. We use the well established mathematical structure of idempotent semirings as the basis for a product family algebra that allows a formal treatment of the above notions. A particular application of the algebra concerns the multi-view reconciliation problem that arises when complex systems are modelled. We use algebraic integration constraints linking features in one view to features in the same or a different view and show in several examples the suitability of this approach for a wide class of integration constraint formulations.
(joint work with R. Khedri and B. Möller)

BernhardMoeller, Concurrent Kleene Algebra: A concurrent Kleene algebra is one which, next to choice and iteration, offers two composition operators, one that stands for sequential execution and the other for concurrent execution. They are related by an inequational form of the exchange/abides law. We show applicability of the algebra to a partially-ordered trace model of program execution semantics and demonstrate its by validating familiar proof rules for sequential programs (Hoare triples) and for concurrent programming (Jones's rely/guarantee calculus). The latter involves an algebraic notion of invariants; for these the exchange inequation strengthens to an equational distributivity law.
(joint work with C.A.R. Hoare, G. Struth and I. Wehrman)

Han-HingDang, Algebraic Aspects of Separation Logic: Over the last four decades a lot of effort has been invested to ensure correctness of programs by using formal specification and verification methods. Some approaches for imperative programming languages have already been introduced by Hoare and Dijkstra to ensure partial or total correctness. But they lack expressiveness for shared mutable data structures, i.e., structures where updatable fields can be referenced from more than one point. Therefore a novel system called separation logic has been developed by John C. Reynolds. Separation logic is an extension of Hoare logic with assertions that express assumptions about separation in storage. Furthermore the command language is enriched by some constructs which allows altering these separate ranges.
We will present another view of separation logic, using an algebraic approach to simplify proofs in this logic. First we will explain the new ideas in separation logic. Especially, we talk about assertions and explain how they can be treated algebraically. Especially for the class of so-called pure assertions we have found an axiomatization from which we were able to prove a lot of laws in a simple, pointfree fashion. The semantics of the commands that reference heap cells is played back to a relational treatment for Hoare logic.

RolandGlueck, An Algebraic Approach to Equivalences, Partitions and Bisimulations: Simulations and bisimulations play an important role in generating policies for transition systems, in model checking and in automata theory. Usually they are defined in a relational way arguing on element level. Schlingloff and Heinle sketched an relational approach to it, Winter proposed a relational algebraic/categorical theory of this topic. Our approach is to embed (bi)simulations together with the related topics of equivalences and partitions in the more general framework of modal semirings, quantales and Kleene algebras.

JohanJeuring, Recognizing strategies: In this talk we use strategies to specify how a wide range of exercises can be solved incrementally, such as bringing a logic proposition to disjunctive normal form, reducing a matrix, or calculating with fractions. With such a strategy, we can automatically generate worked-out solutions, track the progress of a student by inspecting submitted intermediate answers, and report back suggestions in case the student deviates from the strategy. Because we can calculate all kinds of feedback automatically from a strategy specification, it becomes less labor-intensive and less ad-hoc to specify new exercise domains and exercises within that domain. A strategy describes valid sequences of transformation rules that solve the exercise at hand, which turns tracking intermediate steps into a parsing problem. This is a promising view at the problem because it allows us to take advantage of many years of experience in parsing sentences of context-free languages, and transfer this knowledge and technology to the domain of stepwise solving exercises. We will show how we implement a strategy recognizer.

JohanJeuring, Constructing strategies for programming: Learning to program is difficult. To support learning programming, we want to develop an intelligent tutoring systems for learning programming. In this talk we illustrate how to construct strategies for solving programming exercises and how these strategies can be used to automatically support students using an intelligent programming tutor to incrementally develop a program.

Thomas Weigert, Some lessons learned from deploying program transformation-based code generators (30 min): For a number of years, we have used a program-transformation environment to realize UML and SDL designs of large industrial systems through high-performance implementations. In this talk, I want to high-light some of the lessons we had to learn about what worked and what did not work (at least, for us) when attempting to deploy such environment in an industrial environment with real users, developing large, embedded systems. While these are not great pearls of wisdom, nevertheless, we ran afoul of many of these insights, and had to suffer with frustrated users and time-consuming reimplementations.
Background: Inspired by a collaboration with Jim Boyle I had implemented a program transformation system in the early nineties. This system grew over the years into an environment for developing industrial-strength applications consisting of: (i) verification of scenario-based specification by ensuring these are consistent and complete via a hybrid theorem-prover/model checker; (ii) generation of test suites from the scenario specifications; (iii) synthesis of UML designs from the scenario specifications; (iv) weaving of multiple design fragments into a single large design; (v) transformation of these designs into highly optimized C code; and (vi) executing the test suites against that code.

-- JeremyGibbons - 11 May 2009