Practical foundations for programming language / (Record no. 13596)

MARC details
000 -LEADER
fixed length control field 05342nam a2200229Ia 4500
003 - CONTROL NUMBER IDENTIFIER
control field NULRC
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20250520102719.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. Cambridge :
Name of publisher, distributor, etc. Cambridge University Press,
Date of publication, distribution, etc. c2013
300 ## - PHYSICAL DESCRIPTION
Extent xviii, 471 pages ;
Dimensions 26 cm.
365 ## - TRADE PRICE
Price amount USD60.01
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. This book offers a fresh perspective on the fundamentals of programming languages through the use of type theory.
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
Holdings
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 Cost, normal purchase price Total checkouts Full call number Barcode Date last seen Copy number Price effective from Koha item type
    Library of Congress Classification     Gen. Ed. - CCIT LRC - Graduate Studies National University - Manila General Circulation 02/17/2016 Purchased - Amazon 60.01   GC QA 76.7 .H37 2013 c.3 NULIB000011355 05/20/2025 c.3 05/20/2025 Books