资源描述:
《Springer.Using.Understanding.And.Unraveling.The.Ocaml.Language.(Chapter.From.Springer.Applied.Semantics,Lncs.2395).2002》由会员上传分享,免费在线阅读,更多相关内容在学术论文-天天文库。
1、Using,Understanding,andUnravelingtheOCamlLanguageFromPracticetoTheoryandViceVersaDidierR´emyINRIA-Rocquencourthttp://cristal.inria.fr/∼remyAbstract.Thesecoursenotesareaddressedtoawideaudienceofpeo-pleinterestedinmodernprogramminglanguagesingeneral,ML-likelan-guagesinpart
2、icular,orsimplyinOCaml,whethertheyareprogrammersorlanguagedesigners,beginnersorknowledgeablereaders—littlepre-requiresiteisactuallyassumed.Theyprovideaformaldescriptionoftheoperationalsemantics(evalu-ation)andstaticssemantics(typechecking)ofcoreMLandofseveralextensionsst
3、artingfromsmallvariationsonthecorelanguagetoendupwiththeOCamllanguage—oneofthemostpopularincarnationofML—includingitsobject-orientedlayer.Thetightconnectionbetweentheoryandpracticeisaconstantgoal:formaldefinitionsareoftenaccompaniedbyOCamlprograms:aninter-preterfortheoper
4、ationalsemanticsandanalgorithmfortyperecon-structionareincluded.Conversely,somepracticalprogrammingsitua-tionstakenfrommodularorobject-orientedprogrammingpatternsareconsidered,comparedwithoneanother,andexplainedintermsoftype-checkingproblems.Manyexerciseswithdifferentleve
5、lofdifficultiesareproposedallalongtheway,sothatthereadercancontinuouslycheckshisunderstandingandtrainshisskillsmanipulatingthenewconcepts;soon,hewillfeelinvitedtoselectmoreadvancedexercisesandpursuetheexplorationdeepersoastoreachastagewherehecanbeleftonhisown.G.Bartheetal.
6、(Eds.):AppliedSemantics,LNCS2395,pp.413–536,2002.cSpringer-VerlagBerlinHeidelberg2002414DidierR´emyTableofContentsIntroduction...................................................4172CoreML..................................................4212.1DiscoveringCoreML..........
7、................................4212.2TheSyntaxofCoreML........................................4232.3TheDynamicSemanticsofCoreML............................4242.3.1ReductionSemantics......................................4252.3.2PropertiesoftheReduction...................
8、.............4312.3.3Big-StepOperationalSemantics............................4342.4TheStaticSemanticsof