The theory presented here, IOCC (Impredicative theory of Operations, Control, and Classes) is an essentially first-order, two-layered theory. The lower layer is a theory of program equivalence and definedness. Program primitives that can be treated within this theory include functional application and abstraction, conditional, numbers, pairing, and continuation capture and resumption. 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 satisfying systems of equations such as [S = A x G; G = B -> S] which are useful in treating programming concepts such as streams and object behaviors. Coroutines can also be classified within this theory. Examples are given illustrating the derivation of programs using escape mechanisms, and methods for reasoning about streams and coroutines. Methods are given for constructing models of IOCC from semantic models of the underlying programming language.
Keywords: IOCC, functional, control abstraction, program equivalence, specification, transformation, streams, co-routines, induction principles