Abstract
Functional programs often combine separate parts using intermediate data structures for communicating results. Programs so defined 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, and has been studied in the context of both pure and monadic functional programs. In this paper, we study several shortcut fusion extensions, so that, alternatively, circular or higher-order programs are derived. These extensions are also provided for effect-free programs and monadic ones. Our work results in a set of generic calculation rules, that are widely applicable, and whose correctness is formally established. © 2011 Springer Science+Business Media, LLC.

Abstract
Circular functional programs (necessarily evaluated lazily) have been used as algorithmic tools, as attribute grammar implementations, and as target for program transformation techniques. Classically, Richard Bird [1984] showed how to transform certain multi-traversal programs (which could be evaluated strictly or lazily) into one-traversal ones using circular bindings. Can we go the other way, even for programs that are not in the image of his technique? That is the question we pursue in this paper. We develop an approach that on the one hand lets us deal with typical examples corresponding to attribute grammars, but on the other hand also helps to derive new algorithms for problems not previously in reach. © 2011 ACM.

Abstract
This paper describes the embedding of ClassSheet models in spreadsheet systems. ClassSheet models are well-known and describe the business logic of spreadsheet data. We embed this domain specific model representation on the (general purpose) spreadsheet system. By defining such an embedding, we provide end users a model-driven engineering spreadsheet developing environment. End users can interact with both the model and the spreadsheet data in the same environment. Moreover, we use advanced techniques to evolve spreadsheets and models and to have them synchronized. In this paper we present our work on extending a widely used spreadsheet system with such a model-driven spreadsheet engineering environment.

Abstract
Spreadsheets are notoriously error-prone. To help avoid the introduction of errors when changing spreadsheets, models that capture the structure and interdependencies of spreadsheets at a conceptual level have been proposed. Thus, spreadsheet evolution can be made safe within the confines of a model. As in any other model/instance setting, evolution may not only require changes at the instance level but also at the model level. When model changes are required, the safety of instance evolution can not be guarded by the model alone. We have designed an appropriate representation of spreadsheet models, including the fundamental notions of formulteand references. For these models and their instances, we have designed coupled transformation rules that cover specific spreadsheet evolution steps, such as the insertion of columns in all occurrences of a repeated block of cells. Each model-level transformation rule is coupled with instance level migration rules from the source to the target model and vice versa. These coupled rules can be composed to create compound transformations at the model level inducing compound transformations at the instance level. This approach guarantees safe evolution of spreadsheets even when models change.

Abstract
In this paper we present a computer assisted proof of the correctness of a partial derivative automata construction from a regular expression within the Coq proof assistant. Tins proof is part of a formalization of Kleene algebra and regular languages in Coq towards their usage in program certification.

Abstract
This paper is concerned with the scaleable and systematic analysis of interactive systems. The motivating problem is the procurement of medical devices. In such situations several different manufacturers offer solutions that support a particular clinical activity. Apart from cost, which is a dominating factor, the variations between devices are relatively subtle and the consequences of particular design features are not clear from manufacturers' manuals, demonstrations or trial uses. Despite their subtlety these differences can be important to the safety and usability of the device. The paper argues that formal analysis of the range of offered devices can provide a systematic means of comparison. The paper also explores barriers to the use of such techniques, demonstrating how layers of specification may be used to make it possible to reuse common specification. Infusion pumps provide a motivating example. A specific model is described and analysed and comparison between competitive devices is discussed. © Formal Methods for Interactive Systems 2011.