IFIP Working Group 2.1 -- Meeting #62 Details

Contents of this page:    Photos  |  Local information  |  Last-minute details  |  Proposed topics for discussion  |  Proposed talks

Photos

Local information

Hotel "Château de Namur"
Avenue de l'Ermitage, 1
B-5000 Namur, Belgium
Tel + 32 81 72 99 00
Fax + 32 81 72 99 99

In the registration, indicate your special wishes, if any: for instance, you may choose

• to share a twin or double room, and with whom;
• to skip meals, and which ones.

No credit number and no advance payment is needed; but don't cancel your reservation at the last minute.

Here is an estimate of the costs:

(A.1)

Room and breakfast: €97 per person/day. If a twin or double room is shared: €62.5 per person/day.

(A.2)

Lunches (€34) and dinners (€42): €76 per person/day.

(A.3)

Meeting facilities: €95 per participant/week.

(B)

Excursion and banquet: about €50.

A dinner is scheduled at the hotel on Sunday 10 evening; people will be served up to 9 p.m. The banquet is scheduled for Thursday evening.

No lunch is organized on Friday noon; interested people may request this lunch, onMonday morning. If you intend to skip a scheduled meal, and do not want to pay for it, indicate this in your registration, not later.

The hotel is rather isolated. There is one café-restaurant nearby, closed in the evening. One needs around 30 minutes for walking down to the city centre. Note downtownis really "down": the city is at the river level, whereas the hotel is on top of the citadel hill.

There is a Wifi network in the hotel. Access cards for 1 hour (€10), 24 hours (€20) or 5 days (€50) may be purchased. The periods cannot be interrupted, and each card is associated with a unique computer.

If you arrive at Brussels airport, you may take a train to Brussels, then to Namur, and from there a taxi to the hotel. Here are train timetables. The airport station is identified by bruxelles nat airport.

In Namur, there is also a bus (number 3) from the train station to the hotel; the terminus is close to the hotel. This bus runs once per hour, every day. If you travel by car, "unlimited" parking is available, as they say.

Here a few additional links: the hotel, maps, and the city.

For hotel matters, ask the hotel. For general requests, ask Charles Pêcheur; he will help Michel Sintzoff.

Last-minute details

Venue

Schedule

Transportation

Bus route 3 connects the station and the hotel, every hour or so, until 7pm. Past that time, you will have to take a taxi.

Excursion

The visits will cost 8€/person, transportation not included. A registration list will be circulated on Monday.

Banquet

The banquet will cost 40€/person, transportation not included. A registration list will be circulated on Monday.

Weather

Proposed topics for discussion

Proposed talks

Symbolic generation of optimal discrete control (Michel Sintzoff)

The extensional, state-based generation of policies for optimal discrete control is impractical when there are very many states since its complexity is polynomial in the number of states. To avoid this drawback, an intensional approach is proposed: optimal control guards of actions are generated by a symbolic iteration. The domain of states is stratified into domain strata, viz. sets of states having the same optimal value. The optimal guards are stratified into guard strata which are subsets of domain strata. The optimal values are generated by greedy iteration steps. The strata are generated by iteration steps which are guided by the greedy ones and are asynchronous: the guard strata for an action with an increasing cost depend on domain strata with decreasing ranks. The complexity of this symbolic technique is compared to that of symbolic methods for generating domains of discrete reachability.

Test-driven development (Matteo Vaccari)

I would like to introduce the topic of Test Driven Development. It is a simple and pragmatic way of letting the tests drive interactively the development of programs. It's not really research for me, just an everyday practice I found very effective. I think there is room for research into making TDD more effective with mathematical reasoning, or conversely making program derivation more effective with TDD.

From clear specifications to efficient implementations (Annie Liu)

Two major concerns of study rest at the center of computer science: what to compute, and how to compute efficiently. Problem solving involves going from clear specifications for the "what" to efficient implementations for the "how". This is challenging because clear specifications usually correspond to straightforward implementations, not at all efficient, while efficient implementations are usually difficult to understand, not at all clear.

This talk gives an overview of a general and systematic method for transforming clear specifications into efficient implementations. We will present the method through examples, taken from problems in hardware design and image processing expressed using loops and array, in query processing and access control expressed using set operations, in sequence processing and math puzzles expressed using recursive functions, in program analysis and trust management expressed using logic rules, and in building software components expressed using objects. We summarize our ongoing projects on a number of fronts.

Generic and Indexed Programming (Jeremy Gibbons)

At Oxford, we have just started a 42-month EPSRC-funded project on Generic and Indexed Programming, a continuation of the recently-completed Datatype-Generic Programming project. The `indexed' aspect of this project is about expressing more of the structure (specifically, invariants) of a program in the types. We have in mind things like the shape of a data structure, the state of a component, and some property of a represented value. Mechanisms such as Haskell's generalized algebraic datatypes can be used to provide a kind of lightweight dependently-typed programming. Similar ideas are expressible in modern OO languages such as Java and C#. In this talk, I will outline the aims of the project.

(Joint work with Bruno Oliveira.)

Parametric Datatype-Genericity (Jeremy Gibbons)

Datatype-generic programs are programs parametrized by a datatype or type functor. There are two main styles of datatype-generic programming: the Algebra of Programming approach, characterized by structured recursion operators parametrized by a shape functor, and the Generic Haskell approach, characterized by case analysis over the structure of a datatype. We show that the former enjoys a kind of parametricity, relating the behaviours of generic functions at different types; in contrast, the latter is more ad hoc, with no coherence required or provided between the various clauses.

(Joint work with Ross Paterson.)

CancerGrid: Model- and Metadata-Driven Clinical Trials Informatics (Jeremy Gibbons)

The CancerGrid project (www.cancergrid.org) is developing a software architecture for `tissue-plus-data' clinical trials. The project is using a model- and metadata-driven approach that makes the semantics of clinical trials explicit, facilitating dataset discovery and reuse. The architecture is based on open standards for the composition of appropriate services, such as: randomization, minimization, clinician identity, serious adverse events relay, remote data capture, drug allocation and warehousing, form validation.

The project has developed a CONSORT-compliant model for clinical trials, parameterized by clinical data elements hosted in metadata repositories. A model instance can be used to generate and configure services to run the trial it describes. This talk will describe the model, the services, and the technology employed: from XML databases to Office add-ins.

(Joint work with Jim Davies, Steve Harris, and the rest of the CancerGrid team.)

Proving Properties of Constraint Logic Programs by Eliminating Existential Variables (Alberto Pettorossi)

We propose a method for proving first order properties of constraint logic programs which manipulate finite lists of real numbers. Constraints are linear equations and inequations over reals. Our method consists in converting any given first order formula into a stratified constraint logic program and then applying a suitable unfold/fold transformation strategy that preserves the perfect model. Our strategy is based on the elimination of existential variables, that is, variables which occur in the body of a clause and not in its head. Since, in general, the first order properties of the class of programs we consider are undecidable, our strategy is necessarily incomplete. However, experiments show that it is powerful enough to prove several non-trivial program properties.

(Joint work with Maurizio Proietti and Valerio Senni.)

The unfold/fold automatic derivation of winning strategies for solving some impartial games (Alberto Pettorossi)

Polymorphic Algebraic Data Type Reconstruction (Tom Schrijvers - local observer)

Traditional type inference aims at reconstructing type declarations given some type definitions. We present a rule-based constraint rewriting algorithm that reconstructs both type declarations and type definitions.

Our algorithm reconstructs uniform polymorphic definitions of algebraic data types and simultaneously infers the types of all expressions and functions (supporting polymorphic recursion) in the program. The declarative nature of the algorithm allows us to easily show that it has a number of highly desirable properties such as soundness, completeness and various optimality properties. Moreover, we show how to easily extend and adapt it to suit a number of different language constructs and type system features.

Data dependency theory made generic -- by calculation (Jose Nuno Oliveira)

Classical computer science theories (eg. transition systems, parsing, databases) are written pointwise. What do we gain by replaying them in the (relational) pointfree style? This talk will try to answer this question by picking one such widespread theory -- relational database theory (in fact, the data dependency part of it, as far as this talk is concerned) -- and refactoring it in a "let the symbols do the work" style. It can be observed that clear-cut patterns replace long-winded formulae and semi-formal proofs (full of "..." notation, case analyses and English words) give way to compact, agile calculations (namely, that of the "lossless decomposition" theorem); disparate definitions are shown to be equivalent, and so on.

Above all, the theory becomes generic: sets of tuples become binary relations, attributes generalize to arbitrary functions and injectivity is shown to be "what matters" after all. (Also a pro: students like it!)

There are, however, some difficulties. Feedback from the meeting is welcome concerning some hard bits, namely how to make attribute-set complementation (required in some MVD axioms) functional and generic.

Core Role-Based Access Control: Efficient Implementations by Transformations (Annie Liu)

This talk describes a transformational method applied to the core component of role-based access control (RBAC), to derive efficient implementations from a specification based on the ANSI standard for RBAC. The method is based on the idea of incrementally maintaining the result of expensive set operations, where a new method is described and used for systematically deriving incrementalization rules. We calculate precise complexities for three variants of efficient implementations as well as for a straightforward implementation based on the specification. We describe successful prototypes and experiments for the efficient implementations and for automatically generating efficient implementations from straightforward implementations.

Joint work with C. Wang, M. Gorbovitski, T. Rothamel, Y. Cheng, Y. Zhao, and J. Zhang