Practical foundations for programming language / (Record no. 11871)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 06305nam a2200229Ia 4500 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | NULRC |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20250520100712.0 |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 250520s9999 xx 000 0 und d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 9781107029576 |
| 040 ## - CATALOGING SOURCE | |
| Transcribing agency | NULRC |
| 050 ## - LIBRARY OF CONGRESS CALL NUMBER | |
| Classification number | QA 76.7 .H37 2013 |
| 100 ## - MAIN ENTRY--PERSONAL NAME | |
| Personal name | Harper, Robert. |
| Relator term | author |
| 245 #0 - TITLE STATEMENT | |
| Title | Practical foundations for programming language / |
| Statement of responsibility, etc. | Robert Harper. |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. | |
| Place of publication, distribution, etc. | New York : |
| Name of publisher, distributor, etc. | Cambridge University Press, |
| Date of publication, distribution, etc. | c2013 |
| 300 ## - PHYSICAL DESCRIPTION | |
| Extent | xviii, 471 pages : |
| Other physical details | illustrations ; |
| Dimensions | 26 cm |
| 365 ## - TRADE PRICE | |
| Price amount | USD428.29 |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE | |
| Bibliography, etc. note | Includes bibliographical references. |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | Cover; Practical Foundations for Programming Languages; Title; Copyright; Contents; Preface; PART I: Judgments and Rules; 1 Syntactic Objects; 1.1 Abstract Syntax Trees; 1.2 Abstract Binding Trees; 1.3 Notes; 2 Inductive Definitions; 2.1 Judgments; 2.2 Inference Rules; 2.3 Derivations; 2.4 Rule Induction; 2.5 Iterated and Simultaneous Inductive Definitions; 2.6 Defining Functions by Rules; 2.7 Modes; 2.8 Notes; 3 Hypothetical and General Judgments; 3.1 Hypothetical Judgments; 3.1.1 Derivability; 3.1.2 Admissibility; 3.2 Hypothetical Inductive Definitions; 3.3 General Judgments. 3.4 Generic Inductive Definitions3.5 Notes; PART II: Statics and Dynamics; 4 Statics; 4.1 Syntax; 4.2 Type System; 4.3 Structural Properties; 4.4 Notes; 5 Dynamics; 5.1 Transition Systems; 5.2 Structural Dynamics; 5.3 Contextual Dynamics; 5.4 Equational Dynamics; 5.5 Notes; 6 Type Safety; 6.1 Preservation; 6.2 Progress; 6.3 Run-Time Errors; 6.4 Notes; 7 Evaluation Dynamics; 7.1 Evaluation Dynamics; 7.2 Relating Structural and Evaluation Dynamics; 7.3 Type Safety, Revisited; 7.4 Cost Dynamics; 7.5 Notes; PART III: Function Types; 8 Function Definitions and Values; 8.1 First-Order Functions. 8.2 Higher-Order Functions8.3 Evaluation Dynamics and Definitional Equality; 8.4 Dynamic Scope; 8.5 Notes; 9 Godel's T; 9.1 Statics; 9.2 Dynamics; 9.3 Definability; 9.4 Undefinability; 9.5 Notes; 10 Plotkin's PCF; 10.1 Statics; 10.2 Dynamics; 10.3 Definability; 10.4 Notes; PART IV: Finite Data Types; 11 Product Types; 11.1 Nullary and Binary Products; 11.2 Finite Products; 11.3 Primitive and Mutual Recursions; 11.4 Notes; 12 Sum Types; 12.1 Nullary and Binary Sums; 12.2 Finite Sums; 12.3 Applications of Sum Types; 12.3.1 Void and Unit; 12.3.2 Booleans; 12.3.3 Enumerations; 12.3.4 Options. 12.4 Notes13 Pattern Matching; 13.1 A Pattern Language; 13.2 Statics; 13.3 Dynamics; 13.4 Exhaustiveness and Redundancy; 13.4.1 Match Constraints; 13.4.2 Enforcing Exhaustiveness and Redundancy; 13.4.3 Checking Exhaustiveness and Redundancy; 13.5 Notes; 14 Generic Programming; 14.1 Introduction; 14.2 Type Operators; 14.3 Generic Extension; 14.4 Notes; PART V: Infinite Data Types; 15 Inductive and Coinductive Types; 15.1 Motivating Examples; 15.2 Statics; 15.2.1 Types; 15.2.2 Expressions; 15.3 Dynamics; 15.4 Notes; 16 Recursive Types; 16.1 Solving Type Isomorphisms. 16.2 Recursive Data Structures16.3 Self-Reference; 16.4 The Origin of State; 16.5 Notes; PART VI: Dynamic Types; 17 The Untyped -Calculus; 17.1 The -Calculus; 17.2 Definability; 17.3 Scott's Theorem; 17.4 Untyped Means Unityped; 17.5 Notes; 18 Dynamic Typing; 18.1 Dynamically Typed PCF; 18.2 Variations and Extensions; 18.3 Critique of Dynamic Typing; 18.4 Notes; 19 Hybrid Typing; 19.1 A Hybrid Language; 19.2 Dynamics as Static Typing; 19.3 Optimization of Dynamic Typing; 19.4 Static Versus Dynamic Typing; 19.5 Notes; PART VII: Variable Types; 20 Girard's System F; 20.1 System F. Part I. Judgments and rules ; Syntactic objects -- Inductive definitions -- Hypothetical and general judgments -- Part II. Statics and dynamics ; Statics -- Dynamics -- Type safety -- Evaluation dynamics -- Part III. Function types ; Function definitions and values -- G├╢del's T -- Plotkin's PCF -- Part IV. Finite data types ; Product types -- Sum types -- Pattern matching -- Generic programming -- Part V. Infinite data types ; Inductive and coinductive types -- Recursive types -- Part VI. Dynamic types ; The untyped ╬╗-calculus -- Dynamic typing -- Hybrid typing -- Part VII. Variable types ; Girard's System F -- Abstract types -- Constructors and kinds -- Part VIII. Subtyping ; Subtyping -- Singleton kinds -- Part IX. Classes and methods ; Dynamic dispatch -- Inheritance -- Part X. Exceptions and continuations ; Control stacks -- Exceptions -- Continuations -- Part XI. Types and propositions ; Constructive logic -- Classical logic -- Part XII. Symbols ; Symbols -- Fluid binding -- Dynamic classification -- Part XIII. State ; Modernized Algol -- Assignable references -- Part XIV. Laziness ; Lazy evaluation -- Polarization -- Part XV. Parallelism ; Nested parallelism -- Futures and speculations -- Part XVI. Concurrency ; Process calculus -- Concurrent Algol -- Distributed Algol -- Part XVII. Modularity ; Components and linking -- Type abstractions and type classes -- Hierarchy and parameterization -- Part XVIII. Equational reasoning ; Equational reasoning for T -- Equational reasoning for PCF -- Parametricity -- Process equivalence -- Part XIX. Appendix ; Finite sets and finite functions. |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc. | Types are the central organizing principle of the theory of programming languages. In this innovative book, Professor Robert Harper offers a fresh perspective on the fundamentals of these languages through the use of type theory. Whereas most textbooks on the subject emphasize taxonomy, Harper instead emphasizes genetics, examining the building blocks from which all programming languages are constructed. Language features are manifestations of type structure. The syntax of a language is governed by the constructs that define its types, and its semantics is determined by the interactions among those constructs. The soundness of a language design - the absence of ill-defined programs - follows naturally. Professor Harper's presentation is simultaneously rigorous and intuitive, relying on elementary mathematics. The framework he outlines scales easily to a rich variety of language concepts and is directly applicable to their implementation. The result is a lucid introduction to programming theory that is both accessible and practical.--Publisher. |
| 650 ## - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | PROGRAMMING LANGUAGES (ELECTRONIC COMPUTERS) |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) | |
| Source of classification or shelving scheme | Library of Congress Classification |
| Koha item type | Books |
| Withdrawn status | Lost status | Source of classification or shelving scheme | Damaged status | Not for loan | Collection | Home library | Current library | Shelving location | Date acquired | Source of acquisition | Total checkouts | Full call number | Barcode | Date last seen | Copy number | Price effective from | Koha item type |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Library of Congress Classification | Computer Science | LRC - Main | National University - Manila | General Circulation | 05/21/2015 | Purchased - Amazon | GC QA 76.7 .H37 2013 c.2 | NULIB000009630 | 05/20/2025 | c.2 | 05/20/2025 | Books |