Jape is a proof-editor construction kit designed to make it easy to construct visual proof editors with decent user interfaces for more-or-less arbitrary systems of inference. Our goal in building Jape was to make it possible to construct proofs using direct-manipulation interfaces of the kind which can be found in computer-based tools designed to support many other kinds of cognitively hard activity. We also wanted to be able to describe inference systems in a metalanguage no more complicated than that used in everyday logic and computing science texts.
In the first part of this talk we will demonstrate Jape's style of direct-manipulation interface at work in a variety of calculi - including refinement logics, natural semantics, and non-additive sequent calculi. In the second part of the talk we will give an account of the logical and technical infrastructure which supports it. Finally we will argue that a proof tool with a good visual interface cannot be built just by bolting a bit of user-interface technology onto a general purpose proof engine.
The work reported here was done jointly with Richard Bornat of Queen Mary and Westfield College, London University.
The battle is on to define the data socket on the wall in every corner of every room for the home of the future. The socket will be used not just for computers, but telephones, televisions, alarms, answering machines and everything except for basic on/off control of mains appliances. Moreover, the home will be wired to the outside world at high bandwidths, supporting virtual record and video collections, home shopping and home working.
Important physical layer protocols for the wall socket are ATM and Firewire. The speaker will compare the merits of these two solutions, but considering the falling cost of electronics and the capabilities of the two systems, he will also declare whether it is important which contender wins.
The talk is concerned with the use of Massively Parallel Processing (MPP) systems by industry and commerce. In this context, it is argued that the definition of MPP should be extended to include LAN/WAN clusters or 'meta-computers'. The frontier for research for industry has moved on from mere parallel implementations of scientific simulations or commercial databases - rather, it is concerned with the problem of integrating computational and informational resources in a seamless and effective manner. Examples taken from recent research projects at the Parallel Applications Centre (PAC) are used to illustrate these points.
As the cost and size of computers continues to fall, a new generation of `wearable' computers will emerge. Integrated into clothing, worn as jewellery or carried in pockets, wearables will open up new applications and new forms of human-computer interaction. Wearable computers pose new challenges for the computer designer. They will share the wearer's environment, processing sounds and images, and providing communications and location sensing. Their architectures must be optimised for the capture, communication and generation of a wide range of media. They must support software mobility based on mobile processes and mobile communication channels which stretch and contract as the processes and processors move.
In the last few years, a large number of schemes have been proposed for hiding copyright marks and other information in digital pictures, video, audio and other multimedia objects. I will describe some contenders that have appeared in the research literature and in the field; I will then present a number of attacks that enable the information hidden by them to be removed or otherwise rendered unusable.
Over the past ten years, ORL has developed a variety of sensor systems for use indoors. They have been used to observe people and equipment in different ways, and we have explored some of the applications of these technologies. This talk will review the hardware that we have built, explain how the information flows are integrated and made available to applications, and show how these can be regarded as adding a sense of the real world to computer systems.