There are many great references for computer scientists interested in untyped first order logic, such as Melvin Fitting's "First-Order Logic and Automated Theorem Proving" or John Harrison's "Handbook of Practical Logic and Automated Reasoning".
However, I have been having difficulty finding a solid reference that specifically deals with typed (or "many-sorted") first-order logic.
While much knowledge of untyped first-order logic transfers well to a typed setting, there are some interesting questions specific to typed first-order logic that I am interested in seeing a rigorous treatment of, possibly with sample implementations. An obvious example is type-checking, but another is whether it is useful in a typed setting to syntactically distinguish between formulas and terms, or if formulas should just be treated as terms of type
Bool, and the consequences such decisions have on computing normal forms. I'm sure there are other interesting questions as well.
Are there any books you can recommend that have a focus, or even just a lengthy enough chapter, specifically dealing with typed first-order logic?
EDIT: There are some resources listed on Wikipedia for Many-Sorted Logic, however many have to do with Order-Sorted Logic (which is a more sophisticated kind of typed logic than I am looking for, I am only looking for a basic many-sorted logic with disjoint types), or are about one specific kind of algorithm (e.g. Resolution).
One suggestion on there that I like is the first chapter of Calogero G. Zarba's decision theory lecture notes, though it does not really go into the depth I was hoping for and is written more as a summary of definitions, whereas I was hoping more for a thorough book along the lines of Fitting or Harrison.
Perhaps this is too much to hope for as simple many-sorted first-order logic is very similar to untyped first-order logic.