eCite Digital Repository

A Variable Typed Logic of Effects


Honsell, F and Mason, IA and Smith, SF and Talcott, CL, A Variable Typed Logic of Effects, Information and Computation, 119, (1) pp. 55-90. ISSN 0890-5401 (1995) [Refereed Article]

DOI: doi:10.1006/inco.1995.1077


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. © 1995 Academic Press. All rights reserved.

Item Details

Item Type:Refereed Article
Research Division:Information and Computing Sciences
Research Group:Information systems
Research Field:Information systems not elsewhere classified
Objective Division:Information and Communication Services
Objective Group:Other information and communication services
Objective Field:Other information and communication services not elsewhere classified
UTAS Author:Mason, IA (Dr Mason)
ID Code:4707
Year Published:1995
Web of Science® Times Cited:20
Deposited By:Applied Computing and Mathematics
Deposited On:1995-08-01
Last Modified:2011-08-24

Repository Staff Only: item control page