Amazon cover image
Image from Amazon.com

Lambda Calculus with TypesHenk Barendregt, Wil Dekkers, Richard Statman ; with contributions fron Fabio Alessi...[and others.

By: Contributor(s): Material type: TextTextSeries: Publication details: Cambridge : Cambridge University Press, (c)2013.Description: 1 online resource (857 pages)Content type:
  • text
Media type:
  • computer
Carrier type:
  • online resource
ISBN:
  • 9781461936565
Subject(s): Genre/Form: LOC classification:
  • QA9 .L363 2013
Online resources: Available additional physical forms:
Contents:
Subject: This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification.
Tags from this library: No tags from this library for this title. Log in to add tags.
Star ratings
    Average rating: 0.0 (0 votes)
Holdings
Item type Current library Collection Call number URL Status Date due Barcode
Online Book (LOGIN USING YOUR MY CIU LOGIN AND PASSWORD) Online Book (LOGIN USING YOUR MY CIU LOGIN AND PASSWORD) G. Allen Fleece Library ONLINE Non-fiction QA9.5 (Browse shelf(Opens below)) Link to resource Available ocn854975198

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 binary coded decimal

12.2 The filter model mathcal F binary coded decimal12.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 bibliographies and index.

COPYRIGHT NOT covered - Click this link to request copyright permission:

https://lib.ciu.edu/copyright-request-form

There are no comments on this title.

to post a comment.