Contents of this page: Local information | Proposed topics for discussion | Proposed talksMinutes of the meeting are now available (last updated 2nd November 2001).
Description If people are interested, I would be happy to make a presentation on typical industry procedures for generating safety critical certified software. I suspect this is not familiar to a lot of people, and since it sets a framework for the use of formal methods of program construction it seems quite relevant.
Transforming recursion into iteration eliminates the use of stack frames during program execution. It has been studied extensively. This talk describes a powerful and systematic method, based on incrementalization, for transforming general recursion into iteration: identify an input increment, derive an incremental version under the input increment, and form an iterative computation using the incremental version.Exploiting incrementalization yields iterative computation in a uniform way and also allows additional optimizations to be explored cleanly and applied systematically, in most cases yielding iterative programs that use constant additional space, reducing additional space usage asymptotically, and run much faster. I will summarize major optimizations, complexity improvements, and performance measurements. An initial surprise we found is that the classical tail recursive factorial function that uses an accumulating parameter can be slower than the recursive version, even though it eliminates the stack overhead.
This is joint work with Scott Stoller.
This talk presents a marriage between abstract interpretation and theorems-for-free. In brief, we show that various soundness properties of abstract interpretations are in fact "free" theorems derivable by simple type considerations.A simple example is the following. Suppose we use the fold function to sum a list of values:
An "abstract interpretation" of this program might just determine whether the sum is even or not.sum xs = fold 0 (+) xsWe show that the propertyeven(sum xs) = fold True (=) (map even xs)is a free theorem derivable from the type of fold.even(sum xs) <= fold True (=) (map even xs)This example is an elementary instance of the following: Given a type t that is parametric in the type variables a,...,b and an assignment of Galois connections (abs_a,con_a), ..., (abs_b,con_b) to the type variables we show how to construct a Galois connection (abs_t,con_t) and we use this Galois connection to construct a "free" theorem from the type t.
A more substantial example is the abstract interpretation of attribute grammars in order to implement a (sound but not necessarily complete) circularity test.
Practical implications of this result include:
- It can be used to construct abstract interpretations.
- It can be used to focus program testing on those properties that are not for free.
- It suggests a discipline for designing programming language semantics that is able to make better use of developments in generic programming.
This is joint work with Kevin Backhouse.
Danvy has shown how to implement a variant of C's printf
function in a statically typed language. We present a new solution to this
problem based on the notion of a functor. Our solution enjoys nice
algebraic properties and is more direct than the original one.
Along the way, we encounter singleton types, type-indexed values,
type-indexed types, multiple-parameter type classes, and
functional dependencies.
At WG2.1 Meeting 55, I presented necessary and sufficient conditions for when a total function can be written as a fold or as an unfold. I gave a complicated set-theoretic proof of the result.This is joint work with Graham Hutton and Thorsten Altenkirch.Since then, we have generalized the result to partial functions as well. We also have an elegant relational proof, but only of the results for total functions. Curiously, it seems that the relational proof cannot be extended to the partial function generalization. I am hoping for some insight from the group as to why this anomaly arises. (We conjecture that no similar result applies for relations, so it is no surprise that the proof does not apply to relations in general either.)
[HYPERBOLE ON...] Object-oriented programming has failed to live up to its promises of reuse and compositionality: implementation inheritance breaks encapsulation. Component-oriented programming, based on composition and delegation rather than inheritance and overriding, is the way to go. [...HYPERBOLE OFF.]Various groups researching in software architecture, coordination languages, and distributed systems have proposed the separation of computation and coordination as a paradigm for component-oriented programming. Computation is achieved by old-fashioned sequential components; coordination of these components is achieved by the superposition of connectors (first-class entities in their own right) onto the components. Maibaum and Fiadeiro, among others, have shown how to make formal sense of the resulting configurations using pushouts or colimits.
We explain the ideas and motivation, and show how superposition captures exactly what visual application development environments do with technologies like JavaBeans. This is very definitely work in progress.
This presentation is concerned with typed generic higher-order functions of the following kind:A paper draft, the combinator library and generative support for the term interface is readily available at the Strafunski project web page. This is joint work with Joost Visser.These properties are sufficient to define generic function combinators, especially combinators representing traversal schemes. We discuss two models of such generic functions within Haskell. One model is based on universally quantified parameters of datatype constructors. The other one makes hidden use of a universal representation type in a completely safe manner. In both cases, we rely on a very simple term interface.
- The functions can be applied to terms of any type,
- they admit generic traversal into subterms, and
- they also admit type-safe dynamic update.
By contrast, the required form of genericity cannot be achieved with top-level quantified polytypic type parameters as present in PolyP or Generic Haskell. Type cases required for generic function update (see 3 above) are also not supported in those languages.
We present a combinator library for generic functions. We employ our style of generic programming for program transformation, namely for the encoding of program refactorings.
There a recursion scheme for Greedy-like algorithms was based on a a general notion of a `part-of-relation' in monoids. It turns out that this can be generalized in two ways:
- The approach works for general partial orders and offers a simpler treatment of matroids
- We can abstract from relations to elements of Kleene algebras thus making the treatment even more schematic.
Matroids require a fairly strong closure assumption. Therefore they have been generalized to greedoids; these, too, can be dealt with in a simpler fashion using Kleene algebra.
I'll present an introduction to omega algebra (an extension of Kleene algebra to omega-regular languages) and its use in the transformation of concurrent programs.