[Prev][Next][Index][Thread]
New Textbook
PRELIMINARY ANNOUNCEMENT
-------------------------------
The following book will be available shortly:
CATEGORIES FOR TYPES
Cambridge Mathematical Textbooks, Cambridge University
Press ISBN 0521 450926 (HB)
Roy L. Crole, Imperial College, University of London.
Abstract:
This textbook explains the basic principles of
categorical type theory and illustrates some of the
techniques used to derive categorical semantics for
specific type theories. It introduces the reader to
ordered set theory, lattices and domains, and this
material provides plenty of examples for an
introduction to category theory. Categories, functors
and natural transformations are covered, along with the
Yoneda Lemma, cartesian closed categories, limits and
colimits, adjunctions and indexed categories. Four
kinds of formal system are presented in detail, namely
algebraic, functional, second order polymorphic and
higher order polymorphic type theories. For each of
these type theories a categorical semantics is derived
from first principles, and soundness and completeness
results are proved. Correspondences between the type
theories and appropriate categorical structures are
formulated, along with a discussion of internal
languages. Specific examples of categorical models are
given, and in the case of polymorphism both PER and
domain-theoretic structures are considered.
Categorical gluing is used to prove results about type
theories.
Aimed at advanced undergraduates and beginning
graduates, this book will be of interest to theoretical
computer scientists, logicians, and mathematicians
specialising in category theory.
Contents:
(1) Order, Lattices and Domains [1--36]
(2) A Primer on Category Theory [37--119]
(3) Algebraic Type Theory [120--153]
(4) Functional Type Theory [154--196]
(5) Polymorphic Functional Type Theory [197--268]
(6) Higher Order Polymorphism [269--308]
Bibliography [309--313]
Index [314--335]