Ian A. Mason
University of New England
Carolyn L. Talcott
In the 1970s and 1980s Feferman developed several theories for natural formalization of constructive mathematics. These theories treat functions as objects in a first-order setting.
In the 1990s Mason, Talcott and their collaborators used Feferman's theories as a starting point for developing formalisms for reasoning about two specific Landinesque languages: IOCC (Impredicative theory of Operations, Control, and Classes) and VTLoE (Variable Type Logic of Effects). The Landinesque language of IOCC incorporated a control facility similar to Scheme's call/cc, while VTLoE incorporated ML-like reference cells.
Following Feferman's ideas, both formalisms are essentially first-order, two-layered theories. The lower layer is a theory of program equivalence. The upper layer is a theory of class membership with a general comprehension principle for defining classes. Many standard class constructions and data-types can be represented naturally including algebraic abstract data types, list-, record-, and function- type constructions. In addition classes can be constructed as minimal or maximal fix-points, which in turn give rise to associated induction and co-induction principles.
More recently Talcott introduced a general framework for defining the semantics of Landinesque languages along with the notion of uniform semantics. For such languages we have the combined benefits of reduction calculi (modular axiomatization), and operational equivalence (more equations). In addition we have a sound basis for defining satisfaction for VTLoE-style assertions.
In this talk we show how to combine all of these ideas in a logic for reasoning about Landinesque languages called Feferman-Landin logic (FLL for short). FLL generalizes VTLoE to Landinesque languages with uniform semantics. We will give some examples of primitive operations and their formalization in FLL and illustrate some of the subtilties of reasoning about effects as well as the wide range of properties the can be expressed in this logic.