Dov M. Gabbay. Handbooks of logic in computer science. Volume 5

Volume 5.
Logic and Algebraic Methods.
The present Volume 5 continues with logical and algebraic methodologies
basic to computer science. Chapter 1 covers Martin-L0f's type theory,
originally developed to clarify the foundations of constructive mathematics
it now plays a major role in theoretical computer science. The second
chapter covers categorial logic, the interaction area between category theory
and mathematical logic. It builds on the basic concepts introduced
in the chapter 'Basic Category Theory' in Volume 1 of this Handbook series.
The third chapter presents methods for obtaining lower bounds on
the computational complexity of logical theories. Many such theories show
up in the landscape of logic and computation. The fourth chapter covers
algebraic specification and types. It treats the subject using set theoretical
notions only and is thus accessible to a wide range of readers. The last
(fifth) chapter deals with computability on abstract data types. It develops
a theory of computable functions on abstract many-sorted algebras, a
general enough notion for the needs of computer science.