Lambda Calculus with Types / Henk Barendregt, Wil Dekkers, Richard Statman ; with contributions fron Fabio Alessi [and others].

Print version record.

Lambda Calculus with Types; Contents; Preface; Contributors; Our Founders; Introduction; Part I: Simple Types lambda rightarrow mathbb A; 1 The Simply Typed Lambda Calculus; 1.1 The systems lambda rightarrow mathbb A; 1.2 First properties and comparisons; 1.3 Normal inhabitants; 1.4 Representing data types; 1.5 Exercises; 2 Properties; 2.1 Normalization; 2.2 Proofs of strong normalization; 2.3 Checking and finding types; 2.4 Checking inhabitation; 2.5 Exercises; 3 Tools; 3.1 Semantics of lambda rightarrow; 3.2 Lambda theories and term models; 3.3 Syntactic and semantic logical relations.

3.4 Type reducibility3.5 The five canonical term-models; 3.6 Exercises; 4 Definability, unification and matching; 4.1 Undecidability of lambda-definability; 4.2 Undecidability of unification; 4.3 Decidability of matching of rank 3; 4.4 Decidability of the maximal theory; 4.5 Exercises; 5 Extensions; 5.1 Lambda delta; 5.2 Surjective pairing; 5.3 Gödel's system mathcal T: higher-order primitive recursion; 5.4 Spector's system mathcal B: bar recursion; 5.5 Platek's system mathcal Y: fixed point recursion; 5.6 Exercises; 6 Applications; 6.1 Functional programming; 6.2 Logic and proof-checking.

6.3 Proof theory6.4 Grammars, terms and types; Part II: Recursive Types lambda = mathcal A; 7 The Systems lambda = mathcal A; 7.1 Type algebras and type assignment; 7.2 More on type algebras; 7.3 Recursive types via simultaneous recursion; 7.4 Recursive types via mu-abstraction; 7.5 Recursive types as trees; 7.6 Special views on trees; 7.7 Exercises; 8 Properties of Recursive Types; 8.1 Simultaneous recursions vs mu-types; 8.2 Properties of mu-types; 8.3 Properties of types defined by a simultaneous recursion; 8.4 Exercises; 9 Properties of Terms with Types.

9.1 First properties of lambda = mathcal A9.2 Finding and inhabiting types; 9.3 Strong normalization; 9.4 Exercises; 10 Models; 10.1 Interpretations of type assignments in lambda = mathcal A; 10.2 Interpreting Pi mu and Pi mu *; 10.3 Type interpretations in systems with explicit typing; 10.4 Exercises; 11 Applications; 11.1 Subtyping; 11.2 The principal type structures; 11.3 Recursive types in programming languages; 11.4 Further reading; 11.5 Exercises; Part III: Intersection Types lambda cap mathcal S; 12 An Example System; 12.1 The type assignment system lambda cap BCD.

12.2 The filter model mathcal F BCD12.3 Completeness of type assignment; 13 Type Assignment Systems; 13.1 Type theories; 13.2 Type assignment; 13.3 Type structures; 13.4 Filters; 13.5 Exercises; 14 Basic Properties of Intersection Type Assignment; 14.1 Inversion lemmas; 14.2 Subject reduction and expansion; 14.3 Exercises; 15 Type and Lambda Structures; 15.1 Meet semi-lattices and algebraic lattices; 15.2 Natural type structures and lambda structures; 15.3 Type and zip structures; 15.4 Zip and lambda structures; 15.5 Exercises; 16 Filter Models; 16.1 Lambda models; 16.2 Filter models.

16.3 mathcal D infty models as filter models.

This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification.

Includes bibliographical references and index.

eBooks on EBSCOhost EBSCO eBook Subscription Academic Collection - Worldwide