| 000 -LEADER |
|---|
| fixed length control field |
04875mam a2200325 a 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
1486802 |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20260521091923.0 |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
930929s1994 maua b 001 0 eng |
| 010 ## - LIBRARY OF CONGRESS CONTROL NUMBER |
|---|
| LC control number |
93039912 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
0262193493 |
| 035 ## - SYSTEM CONTROL NUMBER |
|---|
| System control number |
(OCoLC)ocm29024695 |
|
|---|
| System control number |
(NNC)1486802 |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
KYUCL |
| Transcribing agency |
KYUC |
| 050 00 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA76.7 |
| Item number |
.S345 1994 |
| 082 00 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
QA76.7 |
| Edition number |
.S345 1994 |
| 100 1# - MAIN ENTRY--PERSONAL NAME |
|---|
| Personal name |
Schmidt, David A., |
| Dates associated with a name |
1953 May 10- |
| 245 14 - TITLE STATEMENT |
|---|
| Title |
The structure of typed programming languages / |
| Statement of responsibility, etc. |
David A. Schmidt. |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Place of publication, distribution, etc. |
Cambridge, Mass. : |
| Name of publisher, distributor, etc. |
MIT Press, |
| Date of publication, distribution, etc. |
c1994. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
xiv, 367 p. : |
| Other physical details |
ill. ; |
| Dimensions |
24 cm. |
| 490 1# - SERIES STATEMENT |
|---|
| Series statement |
Foundations of computing |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE |
|---|
| Bibliography, etc |
Includes bibliographical references (p. [343]-360) and index. |
| 505 2# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
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. |
|
|---|
| Formatted contents note |
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. |
|
|---|
| Formatted contents note |
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. |
|
|---|
| Formatted contents note |
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. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Programming languages (Electronic computers) |
| Source of heading or term |
Computer Science |
| General subdivision |
School of Pure and Applied Sciences |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Foundations of computing. |
| 900 ## - EQUIVALENCE OR CROSS-REFERENCE-PERSONAL NAME [LOCAL, CANADA] |
|---|
| Numeration |
TOC |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) |
|---|
| Source of classification or shelving scheme |
|
| Koha item type |
Long Loan Book |
