Designing the Spectator Experience

Interaction is increasingly a public affair, taking place in our theatres, galleries, museums, exhibitions and on the city streets. This raises a new design challenge for HCI, questioning how a performer s interaction with a computer experienced is by spectators. We examine examples from art, performance and exhibition design, comparing them according to the extent to which they hide, partially reveal, transform, reveal or even amplify a performerts manipulations. We also examine the effects of these manipulations including movements, gestures and utterances that take place around direct input and output. This comparison reveals four broad design strategies: `secretive,' where manipulations and effects are largely hidden; `expressive,' where they are revealed, enabling the spectator to fully appreciate the performer's interaction; `magical,' where effects are revealed but the manipulations that caused them are hidden; and finally `suspenseful,' where manipulations are apparent, but effects only get revealed when the spectator takes their turn.

Integrating SVC and HOL with the PROSPER Toolkit

We describe an integration of the SVC decision procedure with the HOL theorem prover. This integration was achieved using the PROSPER toolkit. The SVC decision procedure operates on rational numbers, an axiomatic theory for which was provided in HOL. The decision procedure also returns counterexamples and a framework has been devised for handling counterexamples in a HOL setting.