Computer Science Seminars Spring Term 1993 (File installed by A.Sloman - 18 Dec 1992) CONTENTS - (Use g to access required sections) -- Alan Sloane Monday 11th Jan 2pm -- David Hogg 12 jan 2 pm -- Angel Pobil 13th January (Room G.13 10.30-11.30) -- Barney Hilken 26th Jan -- Claudio Hermida 5 pm 3rd Feb -- Paul Mukherjee Tuesday 2nd Feb -- Philippa Gardner 11 am 4th Feb -- Luc Beaudoin Tuesday 1st March -- Howard Goodman 16th March -- Alan Sloane Monday 11th Jan 2pm "Architectural Choices in Object-Oriented Programming Environments" =================================================================== Dr Alan Sloane, Senior Staff Engineer, Sun Microsystems Monday, 11th January 1993 at 2.00 pm. Room G12 (C Block), Aston Webb Abstract: Object oriented programming places the developer's focus on the construction of software components, on the specification of the relationships among the classes, objects, and procedures of a system, and on re-use of existing components. Consequently a Programming Environment which supports the object-oriented approach must provide multiple perspectives for viewing and modifying the structure of the system, and must provide a high-degree of integration between the individual tools in the environment. Design choices in OO Programming Environments are ranged along two axes : data integration, and control integration. Data integration is concerned with how to represent program state information which is shared by the tools. Control integration is concerned with how to pass control information among the tools. Programming is, of course, only one stage of the software development process. Thus it is desirable that the Programming Environment's integration framework be open and allow integration of third-party tools, for example for Analysis and Design, and for Testing. The necessity to support multiple perspectives on information naturally leads to an architecture in which individual tools are implemented as a Functional Core and one or many Presentation Components. The Functional Core maintains a semantic model of the system, and the Presentation Components represent views onto that model. Such a structure also allows us to split off shared services, including a Common Command Language composed of control structures and primitives. The control structures are uniform across all tools, but the primitives vary from one tool to another. We illustrate these architectural choices by reference to several research and commercial systems and to on-going work in the Integrated Programming Environments group at Sun, and evaluate the relative strengths and weaknesses of the architectural models. Biographical details: Alan Sloane is a Senior Staff Engineer at Sun Microsystems, where he is Architect for Integrated Programming Environments. Prior to joining Sun he was co-architect of ObjectWorks\C++ at ParcPlace Systems, and designer of the CommonView GUI framework at Glockenspiel. -- David Hogg 12 jan 2 pm Spatio-Temporal Databases from Images For the construction of realistic and detailed virtual worlds, large databases of graphical information are needed. Computer vision may provide a cost effective and powerful means for building such databases. The talk will describe work at Leeds on the extraction of dynamical information from TV image sequences as one component of an automated system for the construction of spatio-temporal world models suitable for graphical reconstruction. Particular issues include the extraction of 3D information from motion trajectories and the fusion of information from multiple views. -- Angel Pobil 13th January (Room G.13 10.30-11.30) Title: AI & Robotics Research at Jaume I University (Spain) Speaker: Angel P. del Pobil Abstract The purpose of this talk is to present current research carried out by the Artificial Intelligence & Robotics Group at the Department of Computer Science of Jaume I University (Spain) in order to detect common interests to talk further about. A survey of the problems we are working on will be presented, including: - Robot motion planning - Task and assembly planning - Spatial reasoning and representations for motion and spatial concepts - Representing visual information for spatial reasoning - Neural networks and its application to motion planning - AI and philosophy Research on these topics is at different stages: I have been working on some of them for several years, while others are merely projects that have just got to move. -- Barney Hilken 26th Jan Speaker: Barney Hilken, University of Manchester Title: Towards a Proof Theory for Rewriting Place: Room G12, Aston Webb Building. Time: 2pm Tuesday 26th Jan Abstract -------- Traditional rewriting theory is based on the relation "t rewrites to u" which is a pre-order on the set of terms. By analogy with logic, we introduce the proof theory of rewriting as the mathematical theory of rewrites, allowing the possibility of several distinct rewrites between t and u, and posing the question of when two such rewrites should be considered equal. In this talk we develop the general theory of rewrites, and show that confluence, strong normalisation and normal forms can be given "proof theoretic" definitions, which have good properties. We also show that the simply-typed lambda calculus with beta reduction and eta expansion has such a proof theory, and is confluent and strongly normalising, and we characterise the normal forms. Although this work is inspired by category theory, and some definitions will be strange to non category theorists, this talk will not be presented in categorical terms. It should therefore be accessible to a fairly wide audience. ALL WELCOME -- Claudio Hermida 5 pm 3rd Feb Speaker: Claudio Hermida, Dept. of Computer Science Edinburgh Univ. Venue: Room G12, Aston Webb Building, 5pm Title: On Fibred Adjunctions and Logical Predicates The speaker says I'll try to avoid being too technical; basically, I will give a brief review of some aspects of categorical logic, since this is the framework in which my research takes place. If time allows I'll mention some of my work. ALL WELCOME - especially anyone interested in the mathematical analysis of forms of computation. Abstract: The notion of fibration is a key concept in the categorical interpretation of (intuitionistic) predicate logics. Logical connectives and quantifiers are then understood in terms of fibred adjunctions. Thus, fibrations provide a suitable framework to deal with (some) logical issues on an abstract level. We will present an important factorisation property for (generalised) fibred adjunctions, which has several relevant applications in semantics, especially in the area of categorical logic mentioned above. In particular, we will show how the notion of logical predicate for the simply typed lambda-calculus arises categorically. This will be achieved by expressing in the internal language of a (suitably structured) fibration the cartesian closed structure of its total category, which we infer from the abovementioned property of fibred adjunctions. Examples of this construction include first-order deliverables (consisting of programs, specifications and correctness proofs) and some notions of logical predicates for domains. ALL WELCOME -- Paul Mukherjee Tuesday 2nd Feb Speaker: Paul Mukherjee (Royal Holloway and Bedford New College) Venue: Room G12, Aston Webb, 2pm Tuesday 2nd Feb Title: Specification and Implementation of real-time safety-critical systems. Abstract: The incidence of the use of computers in real-time safety-critical systems has increased drastically in recent years. Formal techniques are often advocated as a way of increasing our confidence in the software for such systems. In this talk we describe a formal specification language and an implementation language designed specifically for real-time safety-critical systems. We also describe their respective mathematical semantics and explain how these can increase our trust in the dependability of the software. All welcome -- Philippa Gardner 11 am 4th Feb Speaker: Philippa Gardner, Dept of Computer Science, Edinburgh Univ. Venue: Room G12, Aston Webb Building, 11 am Thursday 4th Feb Title: LOGICAL FRAMEWORKS Abstract: Computer Science today contains many examples of logics defined from proof systems. Implementing an interactive proof environment for any such logic is a daunting task: examples of such implementations currently in use include HOL, Lambda, LEGO and NuPrl. It is therefore desirable to seek a framework which unifies the structure common to a wide variety of logics, so that much of this effort in implementation can be expended once and for all. Type theories have emerged as leading candidates for frameworks. In this talk, we motivate this use of type theories and introduce a new type-theoretic framework, called ELF+. The major advantage of ELF+ is that it allows us to give general definitions which capture how well a logic has been represented; such definitions are not possible with other frameworks. The key ideas are illustrated using the simple representation of first-order logic in ELF+. (Knowledge of type theory will not be assumed.) ALL WELCOME -- Luc Beaudoin Tuesday 1st March Speaker: Luc Beaudoin Place: room G12 Aston-Webb building time: Tuesday, 30 February at 2pm Title: An Architecture for the Attention Control Theory of Affect Abstract: Aaron Sloman's Attention Control Theory of Affect aims to explain emotion-like phenomena as mainly bi-products of the processing of motives by resource bounded intelligent agents. I will present an architecture which models the processing of motives in a simulated domain. (Motives will be technically defined, and called "motivators".) The architecture includes (amongst others) processes for generating, evaluating, deciding, scheduling, and executing motivators. The architecture also includes (1) a rapid "intepreter" for allocating "management" processes concerned with motivators and (2) a collection of more elaborate processes for managing deliberation, processes that utilise records of the system's internal state. The architecture allows us to model a variety of (motivational) attentional phenenomena. I intend (in the future!) to use the architecture as a preliminary basis for understanding emotion-like states and obsessive-compulsive disorder. Luc -- Howard Goodman 16th March COMPUTER SCIENCE SEMINAR Venue: Tuesday, 16 March 1993 at 2pm in Room G12 (Aston-Webb Block `C') Title: Functional Programming Using Haskell Speaker: Howard S Goodman (Research Student, Birmingham, Computer Science) ABSTRACT In this talk, I shall discuss the many criticisms of conventional, imperative programming languages, and describe and illustrate how functional languages are superior as tools for writing correct programs. After some discussion of the evolution of functional languages, through the 1980s languages ML and Miranda, I shall concentrate on the new common functional language, Haskell. This will be used to illustrate some general principles of functional programming, before leading on to a brief description of functional input/output. Finally, I shall describe how Haskell is a fully object-oriented programming language, and what this aspect is like to use in practice. Everyone is welcome: the material will be kept as general as possible, and no prior knowledge of functional programming is assumed. ------------------------------------------------------------------------ ... howard.