LACATRE is a real-time multitasking applications design environment. It relies on a graphical language combining the data and control-flow approaches and acts, at the lowest level, as a modelling "overlayer" to off-the-shelf real-time executives. At the Preliminary Design level, the designer can model the result of the specification step in terms of activities using Client/Server-paradygm-based Applicative Objects. A major feature of LACATRE is that it takes advantage of all the potentials of graphical programming to model and verify separately the different running phases of an application (initialisation, ending, normal running, exception handling). Correctness verification is tackled by means of Shaw's CRSM (Communicating Real-Time State Machines). A demonstration of the prototype will close the presentation.
The trading of financial derivatives requires extensive support from computers. Indeed, many derivatives are now so complex that calculating their value is otherwise impossible. New products are being created at a bewildering rate, and to succeed, a trading desk must be able to enter the market very quickly.
Until recently, spreadsheets were the predominant technology used. However, OO analysis and implementation can now offer an alternative which retains their rapidity of development, while adding the control and scalability of more traditional MIS systems, and improving usability - all of which are vital as volumes grow.
Some key aspects of the problem domain are presented, together with an explanation of the difficulties of modelling this domain using conventional analysis. Next, there is a description of the key features of an OO model of the domain. This is followed with a discussion of possible implementation strategies. Finally, a comparison with the spreadsheet alternative will be made.
Optical fibres offer a tantalising amount of spectrum space for transmission, typically 5-20 THz depending upon assumptions, but it remains a matter of debate as to how this should be used to maximum effect. At UCL we have looked at some of the ways it can be accessed using multiple optical carriers and some of the limitations. The talk will review our own work and that of some others in the field.
I will also say a few words about the EE Dept at UCL since it appears we may be seeing more of other, courtesy of the Wolfson Foundation!
It has become clear that there is significant similarity in the hardware underlying both message-passing and distributed shared memory architectures. In addition, similar performance goals (high bandwidth and low latency) are important for both paradigms. We show how it is possible to design a machine that supports both programming approaches efficiently. The Stanford FLASH design is used as an example, both to show what is required to efficiently support these paradigms, as well as to examine the critical performance issues.
This talk will give a brief introduction to the High Performance Computing Facility and its background, and then describe the sort of system that is being installed. The aspects covered will be primarily those that are relevant to its use for scientific 'supercomputing', both hardware and software, but for general interest and background information rather than practical programming. These will cover the already installed vector system as well as the parallel one to be installed in September.
The ability to derive a system's properties from the properties of its components is a requisite for the production of networks, the production of systems from commercial off the shelf products, and the production of verified systems from verified components. This paper extends the compositional framework developed by Abadi and Lamport for functional properties to a class of possibilistic properties, a class which includes a variety of confidentiality, integrity, and availability properties. The extension views these properties as closure properties under a class of trace constructors, called selective interleaving functions, and shows the extent to which each of these closure properties is preserved by a variety of compositional constructs.
The economy and flexibility of the process calculi such as the pi-calculus make them attractive both as an object of theoretical study and as a basis for language design and implementation, in particular for concurrent object-oriented languages. However, such generality has a cost: these systems are rather low level, with correspondingly low-level reasoning techniques.
Static type systems for process calculi can be used to recover useful information about program structure, giving rise to more powerful (and realistic) principles of process equivalence. Two examples are discussed in detail:
* Refining channel types to separate the capabilities of sending and receiving on a given channel allows the type system to track the directionality of information flow in a process system and gives rise to an elegant notion of SUBTYPING. Moreover, if the observer of a pair of processes in the definition of bisimulation is restricted to making only well-typed tests, we obtain a coarser equivalence than usual. We can use this equivalence to justify, for example, the validity of a simple translation of the lambda-calculus into the pi-calculus, which fails if we use an untyped definition of equivalence.
* LINEAR channel types can be used to guarantee that certain communications never interfere with other activity in a system of processes, giving rise to a useful proof technique for bisimulation based on partial confluence. Moreover, the typed variant of bisimulation now disallows observers that make nonlinear tests over linear channels, justifying useful program transformations such as tail-call optimizations.
Purely-functional languages have well-known (or at least much-written-about) advantages, but they tend to suffer from the "closed-world assumption"; that is, if you want *any* use of mutable state, libraries written in other languages, or non-determinism arising from concurrency, then you are totally stuck.
In my talk I'll describe how we have begun to make Haskell a more open language. Using monads we have been able to include mutable state, concurrency, non-determinism, and foreign-language calls, all without competely throwing the baby out with the bathwater.
Using parametricity, we can securely encapsulate imperative algorithms that implement pure functions, guaranteeing that their internal stateful-ness is not externally visible. Intriguingly, this parametricity requires the provision of a (single) constant with a rank-2 polymorphic type.
Everything I describe is implemented in Glasgow Haskell, and is in active use; for example, the Haggis graphical user interface toolkit is built on top of Concurrent Haskell.
I plan to tell you about how large numbers are factoredon computers. I would like you to be able to read current research papers with considerable understanding.
To get to this point, you will have to know a bit of number theory, though no more than what any competent computer scientist would have to know.