PRL Seminars

I will describe 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 represents joint work with Doug Howe.

A preliminary version of this talk was given in the Nuprl seminar last semester.