Handbook of Logic in Computer Science Volume 5: Logic and Algebraic Methods

by Abramsky, S.; Gabbay, Dov. M.; Maibaum, T. S. E.

• ISBN13: 9780198537816
• ISBN10: 0198537816
• Format: Hardcover
• Copyright: 2001-04-05
• Publisher: Oxford University Press

Summary

This handbook volume covers fundamental topics of semantics in logic and computation. The chapters (some monographic in length), were written following years of co-ordination and follow a thematic point of view. The volume brings the reader up to front line research, and is indispensable toany serious worker in the areas.

Table of Contents

List of contributors	xvii
Martin-Lof's type theory	1	(38)
B. Nordstrom
K. Petersson
J. M. Smith
Introduction	1	(3)
Different formulations of type theory	3	(1)
Implementations	4	(1)
Propositions as sets	4	(3)
Semantics and formal rules	7	(9)
Types	7	(2)
Hypothetical judgements	9	(3)
Function types	12	(2)
The type Set	14	(1)
Definitions	15	(1)
Propositional logic	16	(3)
Set theory	19	(13)
The set of Boolean values	20	(1)
The empty set	21	(1)
The set of natural numbers	21	(2)
The set of functions (Cartesian product of a family of sets)	23	(3)
Propositional equality	26	(2)
The set of lists	28	(1)
Disjoint union of two sets	29	(1)
Disjoint union of a family of sets	29	(1)
The set of small sets	30	(2)
The ALF series of interactive editors for type theory	32	(7)
Categorial logic	39	(84)
Andrew M. Pitts
Introduction	40	(3)
Equational logic	43	(7)
Syntactic considerations	44	(1)
Categorical semantics	45	(3)
Internal languages	48	(2)
Categorical datatypes	50	(17)
Disjoint union types	52	(5)
Product types	57	(3)
Function types	60	(2)
Inductive types	62	(3)
Computation types	65	(2)
Theories as categories	67	(10)
Change of category	68	(1)
Clasifying category of a theory	68	(5)
Theory--category correspondence	73	(2)
Theories with datatypes	75	(2)
Predicate logic	77	(23)
Formulas and sequents	77	(1)
Hyperdoctrines	78	(4)
Satisfaction	82	(2)
Propositional connectives	84	(5)
Quantification	89	(4)
Equality	93	(4)
Completeness	97	(3)
Dependent types	100	(23)
Syntactic considerations	101	(6)
Classifying category of a theory	107	(2)
Type-categories	109	(5)
Categorical semantics	114	(5)
Dependent products	119	(4)
Further reading	123