Types_and_Programming_Languages

《Types_and_Programming_Languages》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、TypesandProgrammingLanguagesTypesandProgrammingLanguagesBenjaminC.PierceTheMITPressCambridge,MassachusettsLondon,England©2002BenjaminC.PierceAllrightsreserved.Nopartofthisbookmaybereproducedinanyformbyanyelectronicofmechanicalmeans(includingphotocopying,recording,orinform

2、ationstorageandretrieval)withoutpermissioninwritingfromthepublisher.ThisbookwassetinLucidaBrightbytheauthorusingtheLATEXdocumentpreparationsystem.PrintedandboundintheUnitedStatesofAmerica.LibraryofCongressCataloging-in-PublicationDataPierce,BenjaminC.Typesandprogrammingla

3、nguages/BenjaminC.Piercep.cm.Includesbibliographicalreferencesandindex.ISBN0-262-16209-1(hc.:alk.paper)1.Programminglanguages(Electroniccomputers).I.Title.QA76.7.P542002005.13dc212001044428ContentsPrefacexiii1Introduction11.1TypesinComputerScience11.2WhatTypeSystemsAreGoo

4、dFor41.3TypeSystemsandLanguageDesign91.4CapsuleHistory101.5RelatedReading122MathematicalPreliminaries152.1Sets,Relations,andFunctions152.2OrderedSets162.3Sequences182.4Induction192.5BackgroundReading20IUntypedSystems213UntypedArithmeticExpressions233.1Introduction233.2Syn

5、tax263.3InductiononTerms293.4SemanticStyles323.5Evaluation343.6Notes43viContents4AnMLImplementationofArithmeticExpressions454.1Syntax464.2Evaluation474.3TheRestoftheStory495TheUntypedLambda-Calculus515.1Basics525.2ProgrammingintheLambda-Calculus585.3Formalities685.4Notes7

6、36NamelessRepresentationofTerms756.1TermsandContexts766.2ShiftingandSubstitution786.3Evaluation807AnMLImplementationoftheLambda-Calculus837.1TermsandContexts837.2ShiftingandSubstitution857.3Evaluation877.4Notes88IISimpleTypes898TypedArithmeticExpressions918.1Types918.2The

7、TypingRelation928.3Safety=Progress+Preservation959SimplyTypedLambda-Calculus999.1FunctionTypes999.2TheTypingRelation1009.3PropertiesofTyping1049.4TheCurry-HowardCorrespondence1089.5ErasureandTypability1099.6Curry-Stylevs.Church-Style1119.7Notes11110AnMLImplementationofSim

8、pleTypes11310.1Contexts11310.2TermsandTypes11510.3Typechecking115Contentsvii11SimpleExtensions11