| 000 | 04875mam a2200325 a 4500 | ||
|---|---|---|---|
| 999 |
_c1312 _d1312 |
||
| 001 | 1486802 | ||
| 005 | 20260521091923.0 | ||
| 008 | 930929s1994 maua b 001 0 eng | ||
| 010 | _a 93039912 | ||
| 020 | _a0262193493 | ||
| 035 | _a(OCoLC)ocm29024695 | ||
| 035 | _a(NNC)1486802 | ||
| 040 |
_aKYUCL _cKYUC |
||
| 050 | 0 | 0 |
_aQA76.7 _b.S345 1994 |
| 082 | 0 | 0 |
_aQA76.7 _2.S345 1994 |
| 100 | 1 |
_aSchmidt, David A., _d1953 May 10- |
|
| 245 | 1 | 4 |
_aThe structure of typed programming languages / _cDavid A. Schmidt. |
| 260 |
_aCambridge, Mass. : _bMIT Press, _cc1994. |
||
| 300 |
_axiv, 367 p. : _bill. ; _c24 cm. |
||
| 490 | 1 | _aFoundations of computing | |
| 504 | _aIncludes bibliographical references (p. [343]-360) and index. | ||
| 505 | 2 | _a1. 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. | |
| 505 | 0 | _a3.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. | |
| 505 | 0 | _a5.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. | |
| 505 | 0 | _a7.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. | |
| 650 | 0 |
_aProgramming languages (Electronic computers) _2Computer Science _xSchool of Pure and Applied Sciences |
|
| 830 | 0 | _aFoundations of computing. | |
| 900 | _bTOC | ||
| 942 |
_2lcc _cLLB |
||