# An operational approach to combining classical set theory and functional
programming languages

## Abstract:

We have designed a programming logic based on an integration of
functional programming languages with classical set theory. The logic
merges a classical view of equality with a constructive one by using
equivalence classes, while at the same time allowing computation with
representatives of equivalence classes. Given a programming language
and its operational semantics, a logic is obtained by extending the
language with the operators of set theory and classical logic, and
extending the operational semantics with ``evaluation'' rules for these
new operators. This operational approach permits us to give a generic
design. We give a general formalism for specifying evaluation
semantics, and parameterize our design with respect to languages
specifiable in this formalism. This allows us to prove, once and for
all, important properties of the semantics such as the coherence of the
treatment of equality.

Scott Stoller's Home Page