A Variable Typed Logic of Effects

In this paper we introduce a variable typed logic of effects inspired by the variable type systems of Feferman for purely functional languages. VTLoE (Variable Typed Logic of Effects) is introduced in two stages. The first stage is the first-order theory of individuals built on assertions of equality (operational equivalence à la Plotkin), and contextual assertions. The second stage extends the logic to include classes and class membership. The logic we present provides an expressive language for defining and studying properties of programs including program equivalences, in a uniform framework. The logic combines the features and benefits of equational calculi as well as program and specification logics. In addition to the usual first-order formula constructions, we add contextual assertions. Contextual assertions generalize Hoare′s triples in that they can be nested, they can be used as assumptions, and their free variables can be quantified. They are similar in spirit to program modalities in dynamic logic. We use the logic to establish the validity of the Meyer Sieber examples in an operational setting. The theory allows for the construction of inductively defined sets and derivation of the corresponding induction principles. We hope that classes may serve as a starting point for studying semantic notions of type. Naive attempts to represent ML types as classes fail in the sense that ML inference rules are not valid.