000 02262nam a22003617a 4500
001 sulb-eb0015493
003 BD-SySUS
005 20160405134436.0
008 110225s2013||||enk o ||1 0|eng|d
020 _a9781139032636 (ebook)
020 _z9780521766142 (hardback)
020 _z9781107471313 (paperback)
040 _aUkCbUP
_beng
_erda
_cUkCbUP
050 0 0 _aQA9.5
_b.B365 2013
082 0 0 _a511.35
_223
100 1 _aBarendregt, Henk,
_eauthor.
245 1 0 _aLambda Calculus with Types /
_cHenk Barendregt, Wil Dekkers, Richard Statman.
264 1 _aCambridge :
_bCambridge University Press,
_c2013.
300 _a1 online resource (856 pages) :
_bdigital, PDF file(s).
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
490 0 _aPerspectives in Logic
500 _aTitle from publisher's bibliographic system (viewed on 04 Apr 2016).
520 _aThis handbook with exercises reveals in formalisms, hitherto mainly used for hardware and software design and verification, unexpected mathematical beauty. The lambda calculus forms a prototype universal programming language, which in its untyped version is related to Lisp, and was treated in the first author's classic The Lambda Calculus (1984). The formalism has since been extended with types and used in functional programming (Haskell, Clean) and proof assistants (Coq, Isabelle, HOL), used in designing and verifying IT products and mathematical proofs. In this book, the authors focus on three classes of typing for lambda terms: simple types, recursive types and intersection types. It is in these three formalisms of terms and types that the unexpected mathematical beauty is revealed. The treatment is authoritative and comprehensive, complemented by an exhaustive bibliography, and numerous exercises are provided to deepen the readers' understanding and increase their confidence using types.
650 0 _aLambda calculus
700 1 _aDekkers, Wil,
_eauthor.
700 1 _aStatman, Richard,
_eauthor.
776 0 8 _iPrint version:
_z9780521766142
830 0 _aPerspectives in Logic.
856 4 0 _uhttp://dx.doi.org/10.1017/CBO9781139032636
942 _2Dewey Decimal Classification
_ceBooks
999 _c37337
_d37337