資源描述:
《Types_and_Programming_Languages》由會員上傳分享,免費在線閱讀,更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫。
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