A Case Study in the Specification and Analysis of Design Alternatives for a User Interface:
There is considerable interest within the Human Computer Interaction (HCI) community in the use of media spaces to enhance awareness and interaction between workers in offices or other spatially distributed environments. In addition to the ...
Analysing Cognitive Behaviour using LOTOS and Mexitl:
We argue that cognitive models should be used in analysing the usability of multi-modal human computer interfaces and further, that formal methods can be advantageously applied to such analysis. In pursuing this objective we specify the ...
Formalising a Value-Passing Calculus in HOL:
Milner's value-passing calculus for describing and reasoning about communicating systems is formalised in the HOL proof assistant. Based on a previously defined mechanisation of pure CCS (no data communication, only synchronisation) in HOL, ...
Generalised folds for nested datatypes:
Nested datatypes generalise regular datatypes in much the same way that context-free languages generalise regular ones. Although the categorical semantics of nested types turns out to be similar to the regular case, the fold functions are more ...