Practical.Foundations.for.Programming.Languages.2nd.pdf

发布时间：2022-05-29 发布人：admin 分类：说明书资料大小：28.77M 资料格式：pdf 举报版权申诉

ramissue-9504186-4744300845225004984.pdf-第1页.png

第1页 / 共521页

ramissue-9504186-4744300845225004984.pdf-第2页.png

第2页 / 共521页

ramissue-9504186-4744300845225004984.pdf-第3页.png

第3页 / 共521页

ramissue-9504186-4744300845225004984.pdf-第4页.png

第4页 / 共521页

ramissue-9504186-4744300845225004984.pdf-第5页.png

第5页 / 共521页

ramissue-9504186-4744300845225004984.pdf-第6页.png

第6页 / 共521页

ramissue-9504186-4744300845225004984.pdf-第7页.png

第7页 / 共521页

ramissue-9504186-4744300845225004984.pdf-第8页.png

第8页 / 共521页

Half title

Title

Table of Contents

Preface to the Second Edition

Preface to the First Edition

Part I Judgments and Rules

1 Abstract Syntax

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 Notes

3 Hypothetical and General Judgments

3.1 Hypothetical Judgments

3.2 Hypothetical Inductive Definitions

3.3 General Judgments

3.4 Generic Inductive Definitions

3.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 Total Functions

8 Function Definitions and Values

8.1 First-Order Functions

8.2 Higher-Order Functions

8.3 Evaluation Dynamics and Definitional Equality

8.4 Dynamic Scope

8.5 Notes

9 System T of Higher-Order Recursion

9.1 Statics

9.2 Dynamics

9.3 Definability

9.4 Undefinability

9.5 Notes

Part IV Finite Data Types

10 Product Types

10.1 Nullary and Binary Products

10.2 Finite Products

10.3 Primitive Mutual Recursion

10.4 Notes

11 Sum Types

11.1 Nullary and Binary Sums

11.2 Finite Sums

11.3 Applications of Sum Types

11.4 Notes

Part V Types and Propositions

12 Constructive Logic

12.1 Constructive Semantics

12.2 Constructive Logic

12.3 Proof Dynamics

12.4 Propositions as Types

12.5 Notes

13 Classical Logic

13.1 Classical Logic

13.2 Deriving Elimination Forms

13.3 Proof Dynamics

13.4 Law of the Excluded Middle

13.5 The Double-Negation Translation

13.6 Notes

Part VI Infinite Data Types

14 Generic Programming

14.1 Introduction

14.2 Polynomial Type Operators

14.3 Positive Type Operators

14.4 Notes

15 Inductive and Coinductive Types

15.1 Motivating Examples

15.2 Statics

15.3 Dynamics

15.4 Solving Type Equations

15.5 Notes

Part VII Variable Types

16 System F of Polymorphic Types

16.1 Polymorphic Abstraction

16.2 Polymorphic Definability

16.3 Parametricity Overview

16.4 Notes

17 Abstract Types

17.1 Existential Types

17.2 Data Abstraction

17.3 Definability of Existential Types

17.4 Representation Independence

17.5 Notes

18 Higher Kinds

18.1 Constructors and Kinds

18.2 Constructor Equality

18.3 Expressions and Types

18.4 Notes

Part VIII Partiality and Recursive Types

19 System PCF of Recursive Functions

19.1 Statics

19.2 Dynamics

19.3 Definability

19.4 Finite and Infinite Data Structures

19.5 Totality and Partiality

19.6 Notes

20 System FPC of Recursive Types

20.1 Solving Type Equations

20.2 Inductive and Coinductive Types

20.3 Self-Reference

20.4 The Origin of State

20.5 Notes

Part IX Dynamic Types

21 The Untyped λ-Calculus

21.1 The λ-Calculus

21.2 Definability

21.3 Scott’s Theorem

21.4 Untyped Means Uni-Typed

21.5 Notes

22 Dynamic Typing

22.1 Dynamically Typed PCF

22.2 Variations and Extensions

22.3 Critique of Dynamic Typing

22.4 Notes

23 Hybrid Typing

23.1 A Hybrid Language

23.2 Dynamic as Static Typing

23.3 Optimization of Dynamic Typing

23.4 Static versus Dynamic Typing

23.5 Notes

Part X Subtyping

24 Structural Subtyping

24.1 Subsumption

24.2 Varieties of Subtyping

24.3 Variance

24.4 Dynamics and Safety

24.5 Notes

25 Behavioral Typing

25.1 Statics

25.2 Boolean Blindness

25.3 Refinement Safety

25.4 Notes

Part XI Dynamic Dispatch

26 Classes and Methods

26.1 The Dispatch Matrix

26.2 Class-Based Organization

26.3 Method-Based Organization

26.4 Self-Reference

26.5 Notes

27 Inheritance

27.1 Class and Method Extension

27.2 Class-Based Inheritance

27.3 Method-Based Inheritance

27.4 Notes

Part XII Control Flow

28 Control Stacks

28.1 Machine Definition

28.2 Safety

28.3 Correctness of the K Machine

28.4 Notes

29 Exceptions

29.1 Failures

29.2 Exceptions

29.3 Exception Values

29.4 Notes

30 Continuations

30.1 Overview

30.2 Continuation Dynamics

30.3 Coroutines from Continuations

30.4 Notes

Part XIII Symbolic Data

31 Symbols

31.1 Symbol Declaration

31.2 Symbol References

31.3 Notes

32 Fluid Binding

32.1 Statics

32.2 Dynamics

32.3 Type Safety

32.4 Some Subtleties

32.5 Fluid References

32.6 Notes

33 Dynamic Classification

33.1 Dynamic Classes

33.2 Class References

33.3 Definability of Dynamic Classes

33.4 Applications of Dynamic Classification

33.5 Notes

Part XIV Mutable State

34 Modernized Algol

34.1 Basic Commands

34.2 Some Programming Idioms

34.3 Typed Commands and Typed Assignables

34.4 Notes

35 Assignable References

35.1 Capabilities

35.2 Scoped Assignables

35.3 Free Assignables

35.4 Safety

35.5 Benign Effects

35.6 Notes

36 Lazy Evaluation

36.1 PCF By-Need

36.2 Safety of PCF By-Need

36.3 FPC By-Need

36.4 Suspension Types

36.5 Notes

Part XV Parallelism

37 Nested Parallelism

37.1 Binary Fork-Join

37.2 Cost Dynamics

37.3 Multiple Fork-Join

37.4 Bounded Implementations

37.5 Scheduling

37.6 Notes

38 Futures and Speculations

38.1 Futures

38.2 Speculations

38.3 Parallel Dynamics

38.4 Pipelining with Futures

38.5 Notes

Part XVI Concurrency and Distribution

39 Process Calculus

39.1 Actions and Events

39.2 Interaction

39.3 Replication

39.4 Allocating Channels

39.5 Communication

39.6 Channel Passing

39.7 Universality

39.8 Notes

40 Concurrent Algol

40.1 Concurrent Algol

40.2 Broadcast Communication

40.3 Selective Communication

40.4 Free Assignables as Processes

40.5 Notes

41 Distributed Algol

41.1 Statics

41.2 Dynamics

41.3 Safety

41.4 Notes

Part XVII Modularity

42 Modularity and Linking

42.1 Simple Units and Linking

42.2 Initialization and Effects

42.3 Notes

43 Singleton Kinds and Subkinding

43.1 Overview

43.2 Singletons

43.3 Dependent Kinds

43.4 Higher Singletons

43.5 Notes

44 Type Abstractions and Type Classes

44.1 Type Abstraction

44.2 Type Classes

44.3 A Module Language

44.4 First- and Second-Class

44.5 Notes

45 Hierarchy and Parameterization

45.1 Hierarchy

45.2 Abstraction

45.3 Hierarchy and Abstraction

45.4 Applicative Functors

45.5 Notes

Part XVIII Equational Reasoning

46 Equality for System T

46.1 Observational Equivalence

46.2 Logical Equivalence

46.3 Logical and Observational Equivalence Coincide

46.4 Some Laws of Equality

46.5 Notes

47 Equality for System PCF

47.1 Observational Equivalence

47.2 Logical Equivalence

47.3 Logical and Observational Equivalence Coincide

47.4 Compactness

47.5 Lazy Natural Numbers

47.6 Notes

48 Parametricity

48.1 Overview

48.2 Observational Equivalence

48.3 Logical Equivalence

48.4 Parametricity Properties

48.5 Representation Independence, Revisited

48.6 Notes

49 Process Equivalence

49.1 Process Calculus

49.2 Strong Equivalence

49.3 Weak Equivalence

49.4 Notes

Part XIX Appendices

A Background on Finite Sets

Bibliography

Index

Practical Foundations for Programming Languages This text develops a comprehensive theory of programming languages based on type systems and structural operational semantics. Language concepts are precisely defined by their static and dynamic semantics, presenting the essential tools both intuitively and rigorously while relying on only elementary mathematics. These tools are used to analyze and prove properties of languages and provide the framework for combining and comparing language features. The broad range of concepts includes fundamental data types such as sums and products, polymorphic and abstract types, dynamic typing, dynamic dispatch, subtyping and refinement types, symbols and dynamic classification, parallelism and cost semantics, and concurrency and distribution. The methods are directly applicable to language implementation, to the development of logics for reasoning about programs, and to the formal verification language properties such as type safety. This thoroughly revised second edition includes exercises at the end of nearly every chapter and a new chapter on type refinements. Robert Harper is a professor in the Computer Science Department at Carnegie Mellon University. His main research interest is in the application of type theory to the design and implementation of programming languages and to the mechanization of their meta-theory. Harper is a recipient of the Allen Newell Medal for Research Excellence and the Herbert A. Simon Award for Teaching Excellence, and is an Association for Computing Machinery Fellow.

Practical Foundations for Programming Languages Second Edition Robert Harper Carnegie Mellon University

32 Avenue of the Americas, New York, NY 10013 Cambridge University Press is part of the University of Cambridge. It furthers the University’s mission by disseminating knowledge in the pursuit of education, learning, and research at the highest international levels of excellence. www.cambridge.org Information on this title: www.cambridge.org/9781107150300 © Robert Harper 2016 This publication is in copyright. Subject to statutory exception and to the provisions of relevant collective licensing agreements, no reproduction of any part may take place without the written permission of Cambridge University Press. First published 2016 Printed in the United States of America A catalog record for this publication is available from the British Library. Library of Congress Cataloging in Publication Data Names: Harper, Robert, 1957– Title: Practical foundations for programming languages / Robert Harper, Carnegie Mellon University. Description: Second edition. | New York NY : Cambridge University Press, 2016. | Includes bibliographical references and index. Identifiers: LCCN 2015045380 | ISBN 9781107150300 (alk. paper) Subjects: LCSH: Programming languages (Electronic computers) Classification: LCC QA76.7 .H377 2016 | DDC 005.13–dc23 LC record available at http://lccn.loc.gov/2015045380 ISBN 978-1-107-15030-0 Hardback Cambridge University Press has no responsibility for the persistence or accuracy of URLs for external or third-party Internet Web sites referred to in this publication and does not guarantee that any content on such Web sites is, or will remain, accurate or appropriate.

Contents Preface to the Second Edition Preface to the First Edition Part I Judgments and Rules 1 Abstract Syntax 1.1 1.2 1.3 Abstract Syntax Trees Abstract Binding Trees Notes 2 Inductive Definitions 2.1 2.2 2.3 2.4 2.5 2.6 2.7 Judgments Inference Rules Derivations Rule Induction Iterated and Simultaneous Inductive Definitions Defining Functions by Rules Notes 3 Hypothetical and General Judgments 3.1 3.2 3.3 3.4 3.5 Hypothetical Judgments Hypothetical Inductive Definitions General Judgments Generic Inductive Definitions Notes Part II Statics and Dynamics 4 Statics 4.1 4.2 4.3 4.4 Syntax Type System Structural Properties Notes 5 Dynamics 5.1 5.2 Transition Systems 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 Total Functions 8 Function Definitions and Values 8.1 First-Order Functions 8.2 Higher-Order Functions 8.3 Evaluation Dynamics and Definitional Equality 8.4 Dynamic Scope 8.5 Notes 9 System T of Higher-Order Recursion 9.1 Statics 9.2 Dynamics 9.3 Definability 9.4 Undefinability 9.5 Notes Part IV Finite Data Types 10 Product Types 10.1 Nullary and Binary Products 10.2 Finite Products 10.3 Primitive Mutual Recursion

分享到：

赞收藏

资料库

Practical.Foundations.for.Programming.Languages.2nd.pdf

相关推荐

开发技术

热门标签

最新资料