Advanced Topics in Types and Programming Languages PDF 英文.pdf

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

rhinosinlove-9764058-4744300845225176160.pdf-第1页.png

第1页 / 共589页

rhinosinlove-9764058-4744300845225176160.pdf-第2页.png

第2页 / 共589页

rhinosinlove-9764058-4744300845225176160.pdf-第3页.png

第3页 / 共589页

rhinosinlove-9764058-4744300845225176160.pdf-第4页.png

第4页 / 共589页

rhinosinlove-9764058-4744300845225176160.pdf-第5页.png

第5页 / 共589页

rhinosinlove-9764058-4744300845225176160.pdf-第6页.png

第6页 / 共589页

rhinosinlove-9764058-4744300845225176160.pdf-第7页.png

第7页 / 共589页

rhinosinlove-9764058-4744300845225176160.pdf-第8页.png

第8页 / 共589页

文本预览

Advanced Topics in Types and Programming Languages

Advanced Topics in Types and Programming Languages Benjamin C. Pierce, editor The MIT Press Cambridge, Massachusetts London, England

©2005 Massachusetts Institute of Technology 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 editor and authors using the LATEX document preparation system. Printed and bound in the United States of America. Library of Congress Cataloging-in-Publication Data Advanced topics in types and programming languages / Benjamin C. Pierce, editor. p. cm. Includes bibliographical references and index. ISBN 0-262-16228-8 (hc.: alk. paper) 1. Programming languages (Electronic computers). I. Pierce, Benjamin C. QA76.7.A36 2005 005.13—dc22 200457123 10 9 8 7 6 5 4 3 2 1

Contents Preface ix I Precise Type Analyses 1 1 Substructural Type Systems 3 David Walker 1.1 1.2 1.3 1.4 1.5 1.6 4 Structural Properties 6 A Linear Type System Extensions and Variations An Ordered Type System Further Applications Notes 40 36 17 30 2 Dependent Types 45 David Aspinall and Martin Hofmann 2.1 2.2 2.3 2.4 2.5 2.6 2.7 2.8 2.9 2.10 54 45 Motivations Pure FirstOrder Dependent Types Properties Algorithmic Typing and Equality Dependent Sum Types The Calculus of Constructions Relating Abstractions: Pure Type Systems Programming with Dependent Types Implementation of Dependent Types Further Reading 56 86 50 61 64 71 74 83

vi Contents 3 Eﬀect Types and RegionBased Memory Management 87 Fritz Henglein, Henning Makholm, and Henning Niss 3.1 3.2 3.3 3.4 3.5 3.6 3.7 3.8 90 102 Introduction and Overview 87 Value Flow by Typing with Labels Eﬀects RegionBased Memory Management The Tofte–Talpin Type System Region Inference More Powerful Models for RegionBased Memory Management Practical RegionBased Memory Management Systems 106 114 127 123 133 II Types for LowLevel Languages 137 4 Typed Assembly Language 141 Greg Morrisett 4.1 4.2 4.3 4.4 4.5 4.6 4.7 4.8 146 142 TAL0: ControlFlowSafety The TAL0 Type System TAL1: Simple MemorySafety TAL1 Changes to the Type System Compiling to TAL1 Scaling to Other Language Features Some Real World Issues Conclusions 164 172 175 155 161 167 5 ProofCarrying Code 177 George Necula 5.1 5.2 5.3 5.4 5.5 5.6 5.7 5.8 182 177 Overview of Proof Carrying Code Formalizing the Safety Policy VeriﬁcationCondition Generation Soundness Proof The Representation and Checking of Proofs Proof Generation PCC beyond Types Conclusion 219 187 199 214 216 204

Contents vii III Types and Reasoning about Programs 221 6 Logical Relations and a Case Study in Equivalence Checking 223 Karl Crary 227 224 The Equivalence Problem NonTypeDirected Equivalence Checking TypeDriven Equivalence An Equivalence Algorithm Completeness: A First Attempt Logical Relations A Monotone Logical Relation The Main Lemma The Fundamental Theorem 6.1 6.2 6.3 6.4 6.5 6.6 6.7 6.8 6.9 6.10 Notes 228 232 233 237 236 239 243 7 Typed Operational Reasoning 245 Andrew Pitts 7.1 7.2 7.3 7.4 7.5 7.6 7.7 7.8 247 246 245 Introduction Overview Motivating Examples The Language 253 Contextual Equivalence An Operationally Based Logical Relation Operational Extensionality Notes 261 279 288 225 266 IV Types for Programming in the Large 291 8 Design Considerations for MLStyle Module Systems 293 Robert Harper and Benjamin C. Pierce 298 302 294 Basic Modularity Type Checking and Evaluation of Modules Compilation and Linking Phase Distinction 305 Abstract Type Components Module Hierarchies 317 Signature Families Module Families Advanced Topics 8.1 8.2 8.3 8.4 8.5 8.6 8.7 8.8 8.9 8.10 Relation to Some Existing Languages 8.11 History and Further Reading 343 324 338 307 320 341

分享到：

赞收藏

资料库

Advanced Topics in Types and Programming Languages PDF 英文.pdf

相关推荐

课程资源

热门标签

最新资料