I will be discussing a programming language based on rewriting terms in a certain variant of the Tarski-Givant relation calculus. I will show how Horn-Clause programming, with and without Clark's equality theory, and with constructive negation can be translated into our relational formalism in a way that eliminates all first-order variables, with a net improvement in termination behavior.
I will then discuss recent work to extend the calculus to the more general theory of Allegories of Peter Freyd, a categorical generalization of the relation calculus that easily admits extensions to intuitionistic and higher-order logic. Allegories have been used extensively for code generation and transformation (the Algebra of Programming, Bird & De Moor) and I will discuss how some of their work can be exploited to build-in code transformation into the evaluation process.
I will discuss perspectives on the use of our relation formalism for software design and more expressive languages. The topics include joint work with Peter Freyd (Penn), Michael O'Donnell (Chicago) and Julio Mariño (Madrid).