logo资料库

Types and Programming Languages.pdf

发布时间：2022-06-08 发布人：admin 分类：说明书 资料大小：2.00M 资料格式：pdf 举报 版权申诉
第1页 / 共645页
第2页 / 共645页
第3页 / 共645页
第4页 / 共645页
第5页 / 共645页
第6页 / 共645页
第7页 / 共645页
第8页 / 共645页
资料共645页，剩余部分请下载后查看
    Contents
    3 Untyped Arithmetic Expressions
    4 An ML Implementation of Arithmetic Expression
    5 The Untyped Lambda-Calculus
    6 Nameless Representation of Terms
    7 An ML Implementation of the Lambda-Calculus
    8 Typed Arithmetic Expressions
    9 Simply Typed Lambda-Calculus
    11 Simple Extensions
    12 Normalization
    13 References
    14 Exceptions
    18 Case Study: Imperative Objects
    Types and Programming Languages
    Types and Programming Languages Benjamin C. Pierce The MIT Press Cambridge, Massachusetts London, England
    ©2002 Benjamin C. Pierce All rights reserved. No part of this book may be reproduced in any form by any electronic of mechanical means (including photocopying, recording, or information storage and retrieval) without permission in writing from the publisher. This book was set in Lucida Bright by the author using the LATEX document preparation system. Printed and bound in the United States of America. Library of Congress Cataloging-in-Publication Data Pierce, Benjamin C. Types and programming languages / Benjamin C. Pierce p. cm. Includes bibliographical references and index. ISBN 0-262-16209-1 (hc. : alk. paper) 1. Programming languages (Electronic computers). I. Title. QA76.7 .P54 2002 005.13—dc21 2001044428
    Contents Preface xiii 1 Introduction 1 Types in Computer Science 1.1 1 1.2 What Type Systems Are Good For 1.3 1.4 1.5 Type Systems and Language Design Capsule History Related Reading 10 12 4 9 2 Mathematical Preliminaries 15 2.1 2.2 2.3 2.4 2.5 16 Sets, Relations, and Functions Ordered Sets Sequences Induction Background Reading 18 19 20 15 I Untyped Systems 21 3 Untyped Arithmetic Expressions 23 3.1 3.2 3.3 3.4 3.5 3.6 23 Introduction Syntax 26 Induction on Terms Semantic Styles Evaluation Notes 34 43 29 32
    vi Contents 4 An ML Implementation of Arithmetic Expressions 45 4.1 4.2 4.3 46 Syntax Evaluation The Rest of the Story 47 49 5 The Untyped Lambda-Calculus 51 5.1 5.2 5.3 5.4 52 Basics Programming in the Lambda-Calculus Formalities Notes 68 73 58 6 Nameless Representation of Terms 75 6.1 6.2 6.3 Terms and Contexts Shifting and Substitution Evaluation 80 76 78 7 An ML Implementation of the Lambda-Calculus 83 7.1 7.2 7.3 7.4 83 Terms and Contexts Shifting and Substitution Evaluation Notes 87 88 85 II Simple Types 89 8 Typed Arithmetic Expressions 91 8.1 8.2 8.3 91 Types The Typing Relation Safety = Progress + Preservation 92 9 Simply Typed Lambda-Calculus 99 9.1 9.2 9.3 9.4 9.5 9.6 9.7 99 100 104 Function Types The Typing Relation Properties of Typing The Curry-Howard Correspondence Erasure and Typability Curry-Style vs. Church-Style Notes 111 109 111 95 108 10 An ML Implementation of Simple Types 113 10.1 Contexts 113 10.2 Terms and Types 10.3 Typechecking 115 115
    Contents vii 11 Simple Extensions 117 119 124 121 118 117 Base Types Let Bindings 126 Pairs 11.1 11.2 The Unit Type 11.3 Derived Forms: Sequencing and Wildcards 11.4 Ascription 11.5 11.6 11.7 Tuples 11.8 Records 11.9 11.10 Variants 11.11 General Recursion 11.12 Lists Sums 132 128 129 136 142 146 12 Normalization 149 12.1 Normalization for Simple Types 12.2 Notes 152 149 13 References 153 159 Introduction 13.1 13.2 Typing Evaluation 13.3 Store Typings 13.4 165 13.5 Safety 13.6 Notes 170 153 159 162 14 Exceptions 171 14.1 Raising Exceptions 14.2 Handling Exceptions 14.3 Exceptions Carrying Values 172 173 175 III Subtyping 179 15 Subtyping 181 182 Subsumption Properties of Subtyping and Typing 191 15.1 181 15.2 The Subtype Relation 15.3 15.4 The Top and Bottom Types 15.5 15.6 Coercion Semantics for Subtyping 15.7 15.8 Notes Subtyping and Other Features Intersection and Union Types 207 188 193 200 206
    viii Contents 16 Metatheory of Subtyping 209 16.1 Algorithmic Subtyping 16.2 Algorithmic Typing 16.3 16.4 Algorithmic Typing and the Bottom Type Joins and Meets 210 213 218 17 An ML Implementation of Subtyping 221 Syntax Subtyping 17.1 17.2 17.3 Typing 221 221 222 18 Case Study: Imperative Objects 225 230 229 228 Subtyping Simple Classes 18.1 What Is Object-Oriented Programming? 18.2 Objects 18.3 Object Generators 18.4 229 18.5 Grouping Instance Variables 18.6 18.7 Adding Instance Variables 18.8 Calling Superclass Methods 18.9 Classes with Self 18.10 Open Recursion through Self 235 18.11 Open Recursion and Evaluation Order 18.12 A More Efficient Implementation 18.13 Recap 18.14 Notes 244 245 233 234 231 234 241 19 Case Study: Featherweight Java 247 249 247 Introduction 19.1 19.2 Overview 19.3 Nominal and Structural Type Systems 19.4 Definitions Properties 19.5 19.6 Encodings vs. Primitive Objects 19.7 Notes 254 261 263 262 220 225 237 251
    分享到：
    赞 收藏

    相关推荐

    资料库

    课程资源

    共收录17145份资料，累计13个分类，关注成员有19位，主要包括：PHP,网络管理,网页制作,Java,.Net,数据库,3G/移动开发,C/C++,游戏开发,嵌入式,讲义,软件测试,专业指导

    热门标签

    PHP 网络管理 网页制作 Java .Net 数据库 3G/移动开发 C/C++ 游戏开发 嵌入式 讲义 软件测试 专业指导

    最新资料