000 02309nam a22003378i 4500
001 CR9781139567725
003 UkCbUP
005 20200124160251.0
006 m|||||o||d||||||||
007 cr||||||||||||
008 120808s2014||||enk o ||1 0|eng|d
020 _a9781139567725 (ebook)
020 _z9781107036505 (hardback)
040 _aUkCbUP
_beng
_erda
_cUkCbUP
050 0 0 _aQA9
_b.N37 2014
082 0 0 _a551.3
_223
100 1 _aNederpelt, R. P.
_q(Rob P.),
_eauthor.
245 1 0 _aType theory and formal proof :
_ban introduction /
_cRob Nederpelt, Eindhoven University of Technology, the Netherlands, Herman Geuvers, Radbound University Nijmegen, and Eindhoven University of Technology, the Netherlands.
246 3 _aType Theory & Formal Proof
264 1 _aCambridge :
_bCambridge University Press,
_c2014.
300 _a1 online resource (xxv, 436 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 _aType theory is a fast-evolving field at the crossroads of logic, computer science and mathematics. This gentle step-by-step introduction is ideal for graduate students and researchers who need to understand the ins and outs of the mathematical machinery, the role of logical rules therein, the essential contribution of definitions and the decisive nature of well-structured proofs. The authors begin with untyped lambda calculus and proceed to several fundamental type systems, including the well-known and powerful Calculus of Constructions. The book also covers the essence of proof checking and proof development, and the use of dependent type theory to formalise mathematics. The only prerequisite is a basic knowledge of undergraduate mathematics. Carefully chosen examples illustrate the theory throughout. Each chapter ends with a summary of the content, some historical context, suggestions for further reading and a selection of exercises to help readers familiarise themselves with the material.
650 0 _aType theory.
700 1 _aGeuvers, Herman,
_d1964-
_eauthor.
776 0 8 _iPrint version:
_z9781107036505
856 4 0 _uhttps://doi.org/10.1017/CBO9781139567725
999 _c519550
_d519548