A Typed Functional Calculus With State
Arend Rensink · University of Twente Research Information · 1997
We extend the simple typed -calculus with statements. A statement (which can also be thought of as a method or transition) is an abstraction similar to function abstraction; it can be instantiated by providing it with a source state, whereafter it yields a pair of values consisting of an output value and a target state. We obtain a strongly normalising typed calculus for state-based functional programming. 1 Introduction The motivation for this paper is the investigation of formal foundations for the specification and implementation of concurrent and reactive object-oriented systems. For this purpose, following the work of Nierstrasz et al. [16, 17], we intend to adapt techniques of existing formalisms for the specification of reactive behaviour, such as process algebra or temporal logic, to an object-oriented setting. The large majority of such existing formalisms are based on transition systems, in which the dynamic behaviour is modelled by transitions from source states to target ...