![[MCSDept Piccy]](/images/McsLogoIcon.gif)
We recast Milner's work on finite delay in SCCS by giving a continuous denotational semantics for admissibility of infinite computations on a bifinite domain E. Using Abramsky's SFP domain D for bisimulation we obtain a fully abstract model DE for partial fortification. Thus we may apply Abramsky's Domain Theory in Logical Form to obtain a complete program logic for partial fortification. All the semantic operations are continuous, the model supports a notion of fair parallel and it does not provide a continuous model for unbounded non-determinism.
This talk presents a piece of mathematics which was motivated by Computer Science. The results in the talk can be stated and solved using purely operational techniques (and indeed implemented), but we shall not do that.
It is well known that if a functional type theory is generated from a specified algebraic type theory, the former is a conservative extension of the latter (*). This purely type-theoretic result can be translated into an equivalent category-theoretic statement, and the latter can be proved using a technique from Categorical Logic known as gluing or sconing. [The Type Theory/Category Theory correspondence is reminiscent of the Topology/Group Theory translations found in Algebraic Topology.]
In the talk I shall sketch a proof of the following Theorem: A (simple) type theory containing the types nat, fix, unit, functions, products, computations and coproducts is conservative over a specified algebraic theory. (I shall explain the basic concepts of computation and fix types.)
It transpires that the original gluing construction cannot be used to prove this result. My contribution was to develop a new "gluing style" construction which not only proves the Theorem, but provides for a much simpler proof of the result (*).
Polymorphic type systems offer both type security and flexibility, allowing the definition and use of values which behave uniformly across a range of types. Constructor classes are one attempt to increase the expressiveness of such systems without losing the benefits of effective type inference. Combining overloading in the style of Haskell type classes, and a simple form of higher-order polymorphism, constructor classes encourage the definition and use of general purpose operations that behave uniformly across a range of type constructors. We describe a number of examples, concentrating in particular on the application to programming with monads in a functional language, to illustrate the benefits of a language with support for constructor classes.
Safety-critical systems are used as a motivation for much research in formal methods. It is claimed that to ensure correctness and safety such systems should be formally specified and verified.
We examine to what extent existing formal methods, notations and languages are suitable for this task. In particular we look at the essential common features and issues involved in the design of safety-critical systems and propose a new model and semantics for their representation and analysis.
Use of theorem-proving tools is hampered by the lack of an adequate balance between automation and guidance. Machine assisted theorem proving is often seen as a difficult and involved task. Many researchers are addressing the issue of user control of proof. In this talk I will present a method to integrate useful domain knowledge into the proof process, and a general method to exploit such information for guiding the development of proofs.
An important application area for real-time computing is embedded systems where the computing system provides intelligent control of a mechanical, chemical etc. plant or device. The software requirements for such applications depends heavily on the properties of the plant. These properties are usually investigated by control engineers that base their work on the theory for modelling dynamical systems. However, when the models become complex, this theory has its limits. A promising approach is here to see the plant and the computer as a hybrid system where a piecewise continuous dynamical system interacts with a state machine or automaton implemented by the computer program. This approach is the focus of much research by control theorists and computer scientists in recent years, see e.g. Hybrid Systems, LNCS 736, and Hybrid Systems II, LNCS 999.
Design and implementation of a hybrid controller means that control engineers and programmers needs to cooperate. It is clear that both parties must have a common understanding of hybrid systems models, but it is less clear that it is feasible or even desirable that all participants shall be competent in the techniques for, on one side: system identification and regulator design, and on the other side: design of (distributed) real-time programs.
In order to investigate the facets of such a cooperation we are engaged in a series of experiments with a concrete system that uses mode switched control to improve performance. This talk will use these experiments to introduce hybrid systems, and discuss software requirments, and software architecture for such systems.
Imprecision in real-time computations appears very frequently and takes many forms. For example, time/precision trade-off in processor scheduling, clock drifts in distributed systems and in replication of data in fault tolerant systems. Formal models and their associated development framework/methods must cater for imprecision in such computation. In this talk, the Temporal Agent Model (TAM) will be extended to show how imprecision is modelled and reasoned about. Small case studies will be presented throughout the talk.
In this talk I will discuss some recent developments in the mathematical foundations of programming language semantics. On the one hand, Freyd's categorical analysis of recursively defined defined domains has led to simplified techniques for denotational semantics involving such domains. On the other hand, work of Abramsky, Howe and others on co-inductively defined "applicative bisimulations" has provided quite powerful theories of equivalence of functional programs, defined in terms of their operational semantics. I will tie together some of these developments by describing a certain "logical relation" between the syntax and semantics of lambda calculus which can be used to derive extensionality and continuity properties of operationally-defined program equivalences from corresponding properties of recursively defined domains. The logical relation itself goes back to Plotkin. What is new is the recognition that the relation has a certain property (a "universal property", in category-theoretic terms) which both characterises it uniquely and permits the operationally-based properties to be derived.
In recent years there has been much progress in the use of operationally based methods for reasoning about programs and for program verification. Notions such as contextual equivalence and bisimilarity, which historically are perhaps more usually associated with functional programming and concurrency respectively, have been shown to be very closely connected, and such connections can be seen throughout the functional, concurrent and indeed imperative paradigms. In this paper we show that operational techniques from these three settings also apply in a linear functional setting, by proving that linear contextual equivalence and similarity coincide for a simple linear type theory involving linear function types and tensor types. We conclude by remarking that a similar result still holds true when the operational semantics of the type theory is enriched with a limited form of choice operator and full non-determinism in an untyped setting. In proving these results, we show that similarity is a linear precongruence, the latter being the usual notion of precongruence with restrictions on weakening and substitution.
Recent extensions to process algebra can be used to describe performance or error rate properties of systems. We examine how properties of systems expressed in these algebras can be elicited. Particular attention is given to the ability to describe the behaviour of system components parametrically. We present how analytic formulae for performance properties can be derived from probabilistic process algebraic descriptions, demonstrating how local approximate solutions can be derived for the properties when their exact solutions would be too computationally expensive to evaluate. As an example we derive the performance of an Alternating Bit protocol with respect to its error and retry rates.
![[MCSDept Piccy]](/images/McsTopIcon.gif)