000			02088nam a22003378i 4500
001			CR9781139172707
003			UkCbUP
005			20200124160251.0
006			m|||||o||d||||||||
007			cr||||||||||||
008			111013s1993||||enk o ||1 0|eng|d
020			_a9781139172707 (ebook)
020			_z9780521450928 (hardback)
020			_z9780521457019 (paperback)
040			_aUkCbUP _beng _erda _cUkCbUP
050	0	0	_aQA169 _b.C685 1993
082	0	0	_a511.3 _220
100	1		_aCrole, Roy L., _eauthor.
245	1	0	_aCategories for types / _cRoy L. Crole.
264		1	_aCambridge : _bCambridge University Press, _c1993.
300			_a1 online resource (xvii, 335 pages) : _bdigital, PDF file(s).
336			_atext _btxt _2rdacontent
337			_acomputer _bc _2rdamedia
338			_aonline resource _bcr _2rdacarrier
500			_aTitle from publisher's bibliographic system (viewed on 05 Oct 2015).
520			_aThis textbook explains the basic principles of categorical type theory and 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. which covers categories, functors, natural transformations, the Yoneda lemma, cartesian closed categories, limits, adjunctions and indexed categories. Four kinds of formal system are considered in detail, namely algebraic, functional, polymorphic functional, and higher order polymorphic functional type theory. For each of these the categorical semantics are derived and results about the type systems are proved categorically. Issues of soundness and completeness are also considered. Aimed at advanced undergraduates and beginning graduates, this book will be of interest to theoretical computer scientists, logicians and mathematicians specialising in category theory.
650		0	_aCategories (Mathematics)
650		0	_aLambda calculus.
776	0	8	_iPrint version: _z9780521450928
856	4	0	_uhttps://doi.org/10.1017/CBO9781139172707
999			_c519537 _d519535