Contents of this page: Administrative matters | Technical presentations(Last updated 19th July 2005.)
Unusual as it is for a kestrel to play host to a flock of shorebirds, we found a bountiful suite of hospitality, good food and plenty of it.
Our explorations led us -- without major mishap -- on a zigzag course, and allowed us to take a new tack and view our position from a wider perspective.
I presented 2-3 finger trees, a functional representation of sequences supporting access to the ends in amortised constant time, and concatenation and splitting in time logarithmic in the size of the smaller piece. Representations achieving these bounds have appeared previously, but finger trees are much simpler, as are the operations on them. Further, by defining the split operation in a general form, we obtain a general purpose data structure that can serve as a sequence, priority queue, search tree, priority search queue and more.See slides and paper. This is joint work with Ross Paterson.
Program inversion is a fundamental concept in program transformation. We describe the principles behind an automatic program inverter for a first-order functional language and show the inversion of several programs produced by our system. The core of the system uses a stack-based language, local inversion, and eliminates nondeterminism by applying methods from LR(0) parsing. Joint work with M.Kawabe.See paper.
Information is often organized in a structure used to store, edit, view and search data. This structural information can be described by a type (or schema). There are many applications in which we want to view values of a certain type as values of other types, or transform types to other types. In this talk I give several example situations in which you need type transformations, and I discuss a generic program which, given two types, returns the minimum cost (or distance) transformation between these types.The slides are available.
I often feel the need for `canonical examples' of particular programming paradigms: convincing examples that show the advantages and/or capture the essence of that paradigm. I might want such examples for cocktail party conversation (to explain to laypersons what I do), or for illustrations for students (to clarify the differences between paradigms), or as case studies for testing out new techniques (for example, deriving OO programs). I can easily construct such examples for functional programming, imperative programming, algebraic specifications, and so on; but I don't really have any for object-oriented programming. Why is that?I proposed a variety of explanations and answers.
Participants suggested some other answers.
- It is wrong to ask for neat small examples, because OO only comes into its own on large problems.
- It is wrong to ask for example programs, because OO is really a structuring mechanism orthogonal to the programming paradigm.
- Design patterns? I suggest they are evidence of lack of expressiveness in current OO languages, rather than arguments for OO.
- Point and ColourPoint? I don't think this is a favourable example; I don't want coloured points to turn up in my geometrical proof objects.
- Graphical AWTs? Discrete event simulation? I find these convincing examples, but they are not really small.
- Look for examples of modelling, rather than actual programs; OO is about modelling.
- Give up on trying to derive OO programs; representative applications of OO do not admit simple specifications.
- Think harder about examples of programs structured according to the `real world', such as an Asteroids game.
The discussion was lively, but my initial desires have not been completely satisfied.
No abstract provided.The slides are available.
At Meeting 58 in Rome, I talked about Streaming algorithms or metamorphisms: the fused composition of an unfold after a fold, and useful for various change-of-representation problems. However, the theory I had then was specific to lists. I think I now see how to generalize it; the key observation is that the fold stage should be tail-recursive. I reported on this generalization.The slides are available.
This talk argues that specified blocks have every advantage over the combination of assertions, preconditions, postconditions, invariants, and variants, both for verifying programs, and for program development. They are simpler, more general, easier to write, and they make proofs easier.The slides are available.
We present a rule-based framework for defining and implementing a range of finite trace monitoring logics, including future and past time temporal logic, extended regular expressions, real-time logics, interval logics, forms of quantified temporal logics, and so on. Our logic, Eagle, is implemented as a Java library and involves novel techniques for rule definition, manipulation and execution. Monitoring is done on a state-by-state basis, without storing the execution trace. We explained some subtle features of the algorithm and described its application to software fault protection.The slides are available.
No abstract provided.
See paper.
No abstract provided.
This talk describes AutoSmart, an automatic generator of smart card applets that is being developed at Kestrel Institute. AutoSmart generates programs in Java Card (a version of Java tailored to smart cards) from applet specifications written in SmartSlang, a domain-specific language (also being developed at Kestrel Institute as part of this project) that features high-level constructs for smart card concepts. Before generating the code, AutoSmart performs several consistency checks on the SmartSlang specification, some of which involve automated reasoning. The talk also describes an approach to formally certify the correctness of the generated code (with respect to the input specification) independently from AutoSmart, relying on a very small checker only.The slides are available.
No abstract provided.
No abstract provided.
No abstract provided.
Object abstraction supports the separation of what operations are provided by systems and components from how the operations are implemented, and is essential in enabling the construction of complex systems from components. Unfortunately, clear and modular implementations have poor performance when expensive query operations are repeated, while efficient implementations that incrementally maintain these query results are much more difficult to develop and to understand, because the code blows up significantly and is no longer clear or modular.(This work continued from a talk I gave in the NYC meeting but it has grown significantly: starting with a simple high-level language, completely free of complicated Java stuff; with transformations specified in a powerful rule language; with analysis worked out for sets and objects; and with a prototype, exciting applications and experiements. I mainly discussed these new apsects. The tech report version has been accepted by OOPSLA 2005.)This paper describes a powerful and systematic method that first allows the ``what'' of each component to be specified in a clear and modular fashion and implemented straightforwardly in an object-oriented language; then analyzes the queries and updates, across object abstraction, in the straightforward implementation; and finally derives the sophisticated and efficient ``how'' of each component by incrementally maintaining the results of repeated expensive queries with respect to updates to their parameters. Our implementation and experimental results for example applications in query optimization, role-based access control, etc. demonstrate the effectiveness and benefit of the method.
This talks presents a novel language for querying complex graphs where graph edges may have labels that may have parameters. These graphs easily and naturally capture complex interrelated objects in object-oriented systems and XML data. The language is built on extended regular path expressions, and is easier to use and has greater expressive power than previous query languages. We also describe how to transform queries in this language into Datalog with limited extensions, and how to generate specialized algorithms and complexity formulas from Datalog programs with these extensions.This ongoing work also generalizes our work on parametric regular path queries that appeared in PLDI 2004, but we do not yet have extensive applications and experiments like in the PLDI paper. See technical report.
In 1987, Ramadge and Wonham have initiated a successful approach to the control of discrete event systems (DES). DES are modelled by languages or automata over an alphabet of symbols denoting the events. Control can be language-based (observing events and forbidding some event sequences) or state-based (observing states and forbidding some of them).The talk was about using Kleene algebra with domain (KAD), an extension of Kleene algebra, for calculating controllers for DESs under partial observation. I showed how results of Takai, Kodama and Ushio (1995 to 1998) can be reproduced and generalised. The main generalisations are that the results apply to nondeterministic DES and to arbitrary observability relations (not only equivalence relations). KAD leads to these generalisations without any additional effort.
Because the results are proved in a calculational style, they can more easily be checked than those of standard presentations.
No abstract provided.
No abstract provided.