Categorical investigations have disclosed an algebraic theory for "interval algebras" which looks like it will allow a good part of real analysis to be subsumed in an equational theory. Its intended model is the closed real interval, identifiable in many categories as -- ironically -- a final co-algebra. This later characterization (sometimes referred to as a "coinductive definition") forces the algorithms for much of the structure.

There are a number of completeness theorems, the most interesting of which is a consequence of the remarkable fact that every non-trivial algebra of this finitely presented equational theory has a simple quotient and that any simple algebra appears uniquely as a subalgebra of the intended model. This provides purely algebraic proofs of things such as the Dedekind completion for the reals.

For more information about the Logic and Computation Seminar, please see the seminar web page.