Some people may be interested in reading what Jose Meseguer and I did with variables in equations and deduction, starting around 1981. The final 1985 version discusses some connections with categorical approaches; for example, we point out a flaw in Benabou's work. All this was motivated by the need to reason about abstract data types in Computer Science. @article(complas, title = "Completeness of Many-sorted Equational Logic", author = "Joseph Goguen and Jos\'e Meseguer", year = 1985, journal = "Houston Journal of Mathematics", volume = 11, number = 3, pages = "307--334", note = "Preliminary versions have appeared in: {\it SIGPLAN Notices}, July 1981, Volume 16, Number 7, pages 24--37; SRI Computer Science Lab, Report CSL-135, May 1982; and Report CSLI-84-15, Center for the Study of Language and Information, Stanford University, September 1984") &&&&&&&&&&&&&&&&&&&&&&&&&&&&& Signature File &&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&& Joseph A. Goguen, Professor of Computing Science, Programming Research Group, Oxford University Computing Lab, Wolfson Building, Parks Road, Oxford OX1 3QD, United Kingdom. email: Joseph.Goguen@prg.ox.ac.uk [internet] -- usually also works in the UK, but if not, try Joseph.Goguen@uk.ac.ox.prg phone: 283504 [my office]; 283505 [secy]; 273838 [PRG office]; 273839 [FAX].
From USA, dial 011-44-865-...; from UK, dial (0865)-... ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++