I'm writing a computer science paper, and need to give a formal definition of many-sorted term algebras (which correspond to the abstract syntax of programming languages). I'm having trouble finding a standard development of the theory to use.
So far, I've been giving my own notation for use in the rest of the paper, using the definitions from the book Term Rewriting and All That as a starting point and doing the straightforward generalization to the many-sorted case. However, I suspect I've used a name incorrectly at some point, and really would like to have an existing set of definitions to work with. Anyone know one?