Categorical logic and type theory
type: Item
instance of: scholarly article
title: Categorical logic and type theory
zbMATH Open document ID: 0911.03001
author: Bart Jacobs
published in: Studies in Logic and the Foundations of Mathematics
publication date: 1999-02-11T00:00:00Z
review text: The reviewer's first reaction, on picking up this book, was to wonder what on earth the author had found to say on the subject of categorical logic and type theory that could possibly fill 760 pages. After reading the book, I wonder no longer; but the feeling remains that, if the author had been a little more selective in his choice of material to include, the result could have been a much more readable, and potentially more useful, book. To say this is not to belittle the author's achievement in collecting and organizing a very large body of material in coherent form; however, this is first and foremost an encyclopaedic work, into which specialists will delve with much pleasure and profit, rather than a text from which students (other than the most hardy and determined ones) will readily learn how to use the material. The author considers a wide range of different (typed) logics, beginning with simple typed lambda-calculus, and moving on to first-order and higher-order predicate logic, polymorphic type theory and finally dependent type theory. His aim is to set up a common formalism for these, and for their categorical semantics, which will be truly `modular' in the computer-science sense: that is, each new feature can simply be bolted on to the existing structure as and when it is introduced. This is of course a laudable aim; but it does have the effect of making the early chapters of the book, where one is dealing with comparatively simple structures, harder to read than they might have been, because of all the `fastenings' that have to be put in place for the later additions to bolt on to. The author is scrupulous about explaining the eventual purpose of all these `fastenings' as he goes along, but it does not seem to the reviewer that this makes his account any easier for a beginner to follow. The common theme of the categorical semantics is, rightly, the theory of fibred or indexed categories. At present there is a conspicuous lack of a comprehensive account o…
Mathematics Subject Classification ID: 03-02
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 18B25
Mathematics Subject Classification ID: 18D30
Mathematics Subject Classification ID: 68Q55
zbMATH DE Number: 1250366
zbMATH Keywords: first-order logic
zbMATH Keywords: typed lambda-calculus
zbMATH Keywords: higher-order predicate logic
zbMATH Keywords: polymorphic type theory
zbMATH Keywords: dependent type theory
zbMATH Keywords: categorical semantics
zbMATH Keywords: indexed categories
zbMATH Keywords: fibred categories
zbMATH Keywords: regular categories
zbMATH Keywords: coherent categories
zbMATH Keywords: logoses
zbMATH Keywords: toposes
zbMATH Keywords: effective topos
zbMATH Keywords: complete small category of PERs
zbMATH Keywords: semantics of programming languages
reviewed by: Peter Johnstone
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 1250366