Handbook of Automated Reasoning 
Subtitle: Volume II (Handbook of Automated Reasoning)
Contributors: Alan Robinson (Editor); Andrei Voronkov (Editor)
Publisher: North Holland
Published: June 1, 2001
Language: eng
Number of pages: 1188
ISBN-13: 9780444508126
First sentence: Type theory is a language for formalizing mathematics which was invented by Bertrand Russell [Russell 1908].