Paper Info
Title
A first order logic of effects
Abstract
In this paper we describe some of our progress towards an operational implementation of a modern programming logic. The logic is inspired by the variable type systems of Feferman, and is designed for reasoning about imperative functional programs. The logic goes well beyond traditional programming logics, such as Hoare's logic and Dynamic logic in its expressibility, yet is less problematic to encode into higher order logics. The main focus of the paper is to present an axiomatization of the base first order theory.
Year
DOI
Venue
1997
10.1016/S0304-3975(97)00047-9
Theor. Comput. Sci.
Keywords
DocType
Volume
Theorem proving,Contexts,order logic,Formal methods,λ-calculus,Operational semantics
Journal
185
Issue
ISSN
Citations 
2
Theoretical Computer Science
4
PageRank 
References 
Authors
0.46
26
1
Name
Order
Citations
PageRank
Ian A. Mason179797.47