##
Feferman-Landin Logic

Ian A. Mason

University of New England

iam@turing.une.edu.au

Carolyn L. Talcott

Stanford University

clt@sail.stanford.edu

**Abstract**

In a series of papers in the 1960s Landin proposed that
programming languages should consist of the
lambda calculus augmented by primitives for manipulating data as well as
aspects of a program's environment such as state, control, or interactivity.
We will call such languages ``Landinesque languages''.
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.