Abstract
Coordination in R eo emerges from the composition of the behavioural constraints of the primitives, such as channels, in a component connector. Understanding and implementing R eo, however, has been challenging due to interaction of the channel metaphor, which is an inherently local notion, and the non-local nature of constraint propagation imposed by composition. In this paper, the channel metaphor takes a back seat, and we focus on the behavioural constraints imposed by the composition of primitives, and phrase the semantics of R eo as a constraint satisfaction problem. Not only does this provide a clear intensional description of the behaviour of R eo connectors in terms of synchronisation and data flow constraints, it also paves the way for new implementation techniques based on constraint propagation and satisfaction. In fact, decomposing R eo into constraints provides a new computational model for connectors, which we extend to model interaction with an unknown external world beyond what is currently possible in R eo.

Abstract
The ability to interactively render dynamic scenes with global illumination is one of the main challenges in computer graphics. The improvement in performance of interactive ray tracing brought about by significant advances in hardware and careful exploitation of coherence has rendered the potential of interactive global illumination a reality. However, the simulation of complex light transport phenomena, such as diffuse interreflections, is still quite costly to compute in real time. In this paper we present a caching scheme, termed Instant Caching, based on a combination of irradiance caching and instant radiosity. By reutilising calculations from neighbouring computations this results in a speedup over previous instant radiosity-based approaches. Additionally, temporal coherence is exploited by identifying which computations have been invalidated due to geometric transformations and updating only those paths. The exploitation of spatial and temporal coherence allows us to achieve superior frame rates for interactive global illumination within dynamic scenes, without any precomputation or quality loss when compared to previous methods; handling of lighting and material changes are also demonstrated.

Abstract
This paper describes a study conducted at the University of Nottingham, whose goal was to assess whether the students registered on the first-year module "Mathematics for Computer Scientists" appreciate the calculational method. The study consisted of two parts: "Proof Reading" and "Problem Solving". The goal of "Proof Reading" was to determine what the students think of calculational proofs, compared with more conventional ones, and which are easier to verify; we also assessed how their opinions changed during the term. The purpose of "Problem Solving" was to determine if the methods taught have influenced the students' problem-solving skills. Frequent criticisms of our approach are that we are too formal and that the emphasis on syntactic manipulation hinders students' understanding. Nevertheless, the results show that most students prefer or understand better the calculational proofs. On the other hand, regarding the problem-solving questions, we observed that, in general, the students maintained their original solutions. © 2009 Crown.

Abstract

Abstract
Although cryptographic software implementation is often performed by expert programmers, the range of performance and security driven options, as well as more mundane software engineering issues, still make it a challenge. The use of domain specific language and compiler techniques to assist in description and optimisation of cryptographic software is an interesting research challenge. In this paper we investigate two aspects of such techniques, focusing on Elliptic Curve Cryptography (ECC) in particular. Our constructive results show that a suitable language allows description of ECC based software in a manner close to the original mathematics; the corresponding compiler allows automatic production of an executable whose performance is competitive with that of a hand-optimised implementation. In contrast, we study the worrying potential for na < ve compiler driven optimisation to render cryptographic software insecure. Both aspects of our work are set within the context of CACE, an ongoing EU funded project on this general topic.

Abstract
We propose a generic modelling technique that can be used to extend existing frameworks for theoretical security analysis in order to capture the use of timestamps. We apply this technique to two of the most popular models adopted in literature (Bellare-Rogaway and Canetti-Krawczyk). We analyse previous results obtained using these models in light of the proposed extensions, and demonstrate their application to a new class of protocols. In the timed CK model we concentrate on modular design and analysis of protocols, and propose a more efficient timed authenticator relying on timestamps. The structure of this new authenticator implies that an authentication mechanism standardised in ISO-9798 is secure. Finally, we use our timed extension to the BR model to establish the security of an efficient ISO protocol for key transport and unilateral entity authentication.