資源描述：
《Practical Foundations for Programming Languages》由會(huì)員上傳分享，免費(fèi)在線(xiàn)閱讀，更多相關(guān)內(nèi)容在行業(yè)資料-天天文庫(kù)。
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.Thesyntaxofalanguageisgovernedbytheconstructsthatde?neitstypes,anditssemanticsisdeterminedbytheinteractionsamongthoseconstructs.Thesoundnessofalanguagedesign—theabsenceofill-de?nedprograms—followsnaturally.Thepurposeofth
4、isbookistoexplainthisremark.Avarietyofpro-gramminglanguagefeaturesareanalyzedintheunifyingframeworkoftypetheory.Alanguagefeatureisde?nedbyitsstatics,therulesgovern-ingtheuseofthefeatureinaprogram,anditsdynamics,therulesde?ninghowprogramsusingthisfeaturearetobeexecute
5、d.Theconceptofsafetyemergesasthecoherenceofthestaticsandthedynamicsofalanguage.Inthiswayweestablishafoundationforthestudyofprogramminglanguages.Butwhytheseparticularmethods?Themainjusti?cationisprovidedbythebookitself.Themethodsweusearebothpreciseandin-tuitive,provid
6、ingauniformframeworkforexplainingprogramminglan-guageconcepts.Importantly,thesemethodsscaletoawiderangeofpro-gramminglanguageconcepts,supportingrigorousanalysisoftheirprop-erties.Althoughitwouldrequireanotherbookinitselftojustifythisas-sertion,thesemethodsarealsoprac
7、ticalinthattheyaredirectlyapplicabletoimplementationanduniquelyeffectiveasabasisformechanizedreasoning.Nootherframeworkoffersasmuch.Beingaconsolidationanddistillationofdecadesofresearch,thisbookdoesnotprovideanexhaustiveaccountofthehistoryoftheideasthatin-formit.Suf?
8、ceittosaythatmuchofthedevelopmentisnotoriginal,butratherislargelyareformulationofwhathasgonebefore.Thenotesattheendofeachchaptersig
