[Home] [CV] [Publications]

# Publications

A theory of classes for a functional language with effects
- 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.