[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 A theory of classes for a functional language with effects
Honsell, F. and Mason, I. A. and Smith, S. F. and Talcott, C. L. - 1993

In this paper we introduce a variable typed logic of effects (i.e. a logic of effects where classes can be defined and quantified over) inspired by the variable type systems of FefermanĀ \citefeferman-85vt,feferman-90poly for purely functional languages. A similar extension incorporating non-local control operations was introduced inĀ \citetalcott-90disco. The logic we present provides an expressive language for defining specifications and constraints and for studying properties and program equivalences, in a uniform framework. Thus it has an advantage over a number of systems in the literature that aim to capture solitary aspects of computation. The theory also allows for the construction of inductively defined sets and derivation of the corresponding induction principles. Classes can be used to express various effects, including: non-expansiveness of terms; read/write effects and various forms of interference.