Lambda Calculus with Types

"This 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."--Publisher's website Contents......Page 5 Preface......Page 9 Introduction......Page 15 P1......Page 23 1 The Simply Typed Lambda Calculus......Page 27 2 Properties......Page 77 3 Tools......Page 116 4 Definability, unification and matching......Page 214 5 Extensions......Page 265 6 Applications......Page 345 P2......Page 399 7 The Systems......Page 401 8 Properties of Recursive Types......Page 473 9 Properties of Terms with Types......Page 516 10 Models......Page 542 11 Applications......Page 576 P3......Page 599 12 An Example System......Page 601 13 Type Assignment Systems......Page 613 14 Basic Properties of Intersection Type Assignment......Page 641 15 Type and Lambda Structures......Page 662 16 Filter Models......Page 702 17 Advanced Properties and Applications......Page 750 References......Page 813 Index of terms......Page 837 Index of Citations......Page 845 Index of symbols......Page 850 This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification