An algebraic specification of a reflective language

A formal, algebraic specification is presented for a functional programming language, called Brown, with reflective computation mechanisms. The emphasis is put on how it is possible to specify the reflection abstractly (in the sense of abstract data types) in equational logic. The major part of the specification consists of a set of equations (axioms ) based on a denotational semantics which model environment, continuation and metacontinuation. The specification is executable by term rewriting, because the equations can be regarded as the rewrite rules which replace instances of the left-hand sides with the corresponding instances of the right-hand sides