04875mam a2200325 a 4500 1312 1312 1486802 20260521091923.0 930929s1994 maua b 001 0 eng 93039912 0262193493 (OCoLC)ocm29024695 (NNC)1486802 KYUCL KYUC QA76.7 .S345 1994 QA76.7 .S345 1994 Schmidt, David A., 1953 May 10- The structure of typed programming languages / David A. Schmidt. Cambridge, Mass. : MIT Press, c1994. xiv, 367 p. : ill. ; 24 cm. Foundations of computing Includes bibliographical references (p. [343]-360) and index. 1. The Programming Language Core. 1.1. A Core Imperative Language. 1.2. Typing Rules. 1.3. Induction and Recursion. 1.4. Unicity of Typing. 1.5. The Typing Rules Define the Language. 1.6. The Semantics of the Core Language. 1.7. Soundness of the Typing Rules. 1.8. Operational Properties of the Semantics. 1.9. The Design of a Language Core -- 2. The Abstraction Principle. 2.1. Expression Abstractions. 2.2. The Semantics of Abstractions. 2.3. Soundness of the Typing Rules for Abstractions. 2.4. Lazy Evaluation and the Copy Rule. 2.5. Eager Evaluation. 2.6. Semantics of Lazy and Eager Evaluation. 2.7. Other Standard Abstractions. 2.8. Recursively Defined Abstractions. 2.9. Variable Declarations. 2.10. Semantics of Variables. 2.11. Type-Structure Abstractions. 2.12. Semantics of Type Structures. 2.13. Declaration Abstractions. 2.14. The Abstraction Principle Is a Record Introduction Principle -- 3. The Parameterization and Correspondence Principles. 3.1. Expression Parameters. 3.2. Semantics of Parameter Transmission. 3.3. A Copy Rule for Lazily Evaluated Parameters. 3.4. Other Varieties of Parameters. 3.5. Type Equivalence. 3.6. Type-Structure Parameters. 3.7. The Correspondence Principle. 3.7.1. The Semantics of Correspondence. 3.8. Parameter Lists. 3.9. The Parameterization Principle Is a Lambda Abstraction Principle -- 4. The Qualification Principle. 4.1. Command Blocks. 4.1.1. Semantics of the Command Block. 4.2. Scope. 4.2.1. Semantics of Dynamic Scoping. 4.3. Extent. 4.4. Declaration Blocks. 4.5. Type-Structure Blocks. 4.6. Object-Oriented Languages. 4.6.1. Semantics of Dynamically Scoped Objects. 4.7. Subtyping. 4.8. The Copy Rule for Blocks. 4.9. The Qualification Principle Is a Record Introduction Principle -- 5. Records and Lambda Abstractions. 5.1. The Desugared Programming Language. 5.2. Record Introduction. 5.3. Lambda Abstraction Introduction. 5.4. Higher-Order Programming Languages. 5.5. The Semantics of Records and Lambda Abstractions. 5.5.1. Lazy Evaluation Semantics. 5.5.2. Eager Evaluation Semantics. 5.6. Lazy and Eager Evaluation Combined. 5.7. Lambda Abstraction Alone. 5.8. Orthogonality. 5.9. The Model of the Programming Language. 5.10. The Logic of the Programming Language -- 6. The Lambda Calculus. 6.1. The Untyped Lambda Calculus. 6.2. Call-by-Name and Call-by-Value Reduction. 6.3. An Induction Principle. 6.4. The Simply Typed Lambda Calculus. 6.5. Denotational Semantics and Soundness. 6.6. Lambda Calculus with Constants and Operators. 6.7. Operational Semantics for a Source Language. 6.8. Subtree Replacement Systems. 6.9. Standardization -- 7. Functional Programming Languages. 7.1. The Core Functional Language. 7.2. Rewriting Rules for the Core Language. 7.3. The Abstraction and Qualification Principles. 7.4. The Parameterization Principle. 7.5. Denotational Semantics of the Functional Language. 7.5.1. PCF and Computational Adequacy. 7.6. Type Abstractions. 7.7. Variations on Type Abstractions. 7.8. Type Parameters. 7.9. Semantics of Type Abstractions and Type Parameters. 7.10. Type Inference. 7.11. Prolog and Logic Programming Languages -- 8. Higher-Order Typed Lambda Calculi. 8.1. The Second-Order Lambda Calculus. 8.2. Parameterized Data Types. 8.3. Generalized Type Systems. 8.4. Dependent Product Types. 8.5. Dependent Sum Types -- 9. Propositional-Logic Typing. 9.1. The Propositional Calculus. 9.2. Proofs as Programs. 9.3. Programming in the Logic. 9.4. Computing in the Logic. 9.5. Disjunction and Falsehood. 9.6. Classical and Intuitionistic Logic. 9.7. Propositional Logic and Programming-Language Design -- 10. Predicate-Logic Typing. 10.1. The Predicate Calculus. 10.2. The Typed Predicate Calculus with Natural Numbers. 10.3. Universes. 10.4. The Equality Type. 10.5. General Forms of Elimination Rules. 10.6. Technical Results. 10.7. Predicate Logic and Programming-Language Design. Programming languages (Electronic computers) Computer Science School of Pure and Applied Sciences Foundations of computing. TOC lcc LLB 0 0 lcc 0 0 NFIC KyUCL KyUCL 2015-08-10 PURCHASE 3500.00 QA76.7.S345 1994 KYUC/2008/1947 2015-08-10 2015-08-10 LLB