资源描述：
《Practical Foundations for Programming Languages》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、PracticalFoundationsforProgrammingLanguagesRobertHarperCarnegieMellonUniversity[Version1.32of05.15.2012.]Copyrightc2012byRobertHarper.AllRightsReserved.TheelectronicversionofthisworkislicensedundertheCre-ativeCommonsAttribution-Noncommercial-NoDerivativeWorks3.0Unite
2、dStatesLicense.Toviewacopyofthislicense,visithttp://creativecommons.org/licenses/by-nc-nd/3.0/us/orsendalettertoCreativeCommons,171SecondStreet,Suite300,SanFrancisco,California,94105,USA.PrefaceTypesarethecentralorganizingprincipleofthetheoryofprogramminglanguages.La
3、nguagefeaturesaremanifestationsoftypestructure.Thesyntaxofalanguageisgovernedbytheconstructsthatdefineitstypes,anditssemanticsisdeterminedbytheinteractionsamongthoseconstructs.Thesoundnessofalanguagedesign—theabsenceofill-definedprograms—followsnaturally.Thepurposeofth
4、isbookistoexplainthisremark.Avarietyofpro-gramminglanguagefeaturesareanalyzedintheunifyingframeworkoftypetheory.Alanguagefeatureisdefinedbyitsstatics,therulesgovern-ingtheuseofthefeatureinaprogram,anditsdynamics,therulesdefininghowprogramsusingthisfeaturearetobeexecute
5、d.Theconceptofsafetyemergesasthecoherenceofthestaticsandthedynamicsofalanguage.Inthiswayweestablishafoundationforthestudyofprogramminglanguages.Butwhytheseparticularmethods?Themainjustificationisprovidedbythebookitself.Themethodsweusearebothpreciseandin-tuitive,provid
6、ingauniformframeworkforexplainingprogramminglan-guageconcepts.Importantly,thesemethodsscaletoawiderangeofpro-gramminglanguageconcepts,supportingrigorousanalysisoftheirprop-erties.Althoughitwouldrequireanotherbookinitselftojustifythisas-sertion,thesemethodsarealsoprac
7、ticalinthattheyaredirectlyapplicabletoimplementationanduniquelyeffectiveasabasisformechanizedreasoning.Nootherframeworkoffersasmuch.Beingaconsolidationanddistillationofdecadesofresearch,thisbookdoesnotprovideanexhaustiveaccountofthehistoryoftheideasthatin-formit.Suffi
8、ceittosaythatmuchofthedevelopmentisnotoriginal,butratherislargelyareformulationofwhathasgonebefore.Thenotesattheendofeachchaptersig
