资源描述：
《A Concurrent Model for Linear Logic》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。
1、ElectronicNotesinTheoreticalComputerScience155(2006)147–168www.elsevier.com/locate/entcsAConcurrentModelforLinearLogicEmmanuelBeffaraPPS,UniversitéParis7&CNRSAbstractWebuildarealizabilitymodelforlinearlogicusinganame-passingprocesscalculus.Theconstruc-tionisbasedontestingsema
2、nticsforprocesses,drawingideasfromspatialandmodallogics,andyieldsanewtypesystemforprocesscalculithatensuresterminationwhileallowingsignificantlyconcurrentbehaviours.Thenwestudyhowembeddingsofintuitionisticandclassicallogicsintolinearlogicinducetypedtranslationsofλandλμcalculi
3、inwhichnewconcurrentinstructionscanbeintroduced,thussketchingthebasisforaCurry-Howardinterpretationoflinearandclassicalproofsintermsofconcurrentinteraction.Keywords:Linearlogic,π-calculus,proofsasprocesses.1IntroductionThispaperaddressestheproblemoffindingaproperandmeaningful
4、connec-tionbetweenlinearlogicandconcurrencyinthetraditionoftheCurry-Howardisomorphism.Tothisend,wedevelopalogicofbehaviouralpropertiesofpro-cesses,usingideasfromspatialandmodallogics,yieldinganinterpretationofthelogicasatypesystemforprocesses.Sincetheinceptionoflinearlogic[1
5、4],therehavebeenseveralattemptsatprovidingitwithacanonicalcomputationalcounterpart,thesamewayasλ-calculusisacomputationalrepresentationofcoreintuitionisticlogic.Proof-nets,whicharecanonicalproofobjectsforlinearlogic,haveseveralmeaningfulcomputationalintuitions,notablyaboutpa
6、rallelismandresourcemanagement,buttheyaretoocloselyrelatedtologicandprooftheorytobeusedasabasiccomputationalobjectbythemselves.Nevertheless,thoseintuitionspromotedthekeyideasofcomputationbyinteraction,leadingno-tablytothegeneralapproachofgamesemantics,whichsharesmanyintuitio
7、ns1571-0661/$–seefrontmatter©2006ElsevierB.V.Allrightsreserved.doi:10.1016/j.entcs.2005.11.055148E.Beffara/ElectronicNotesinTheoreticalComputerScience155(2006)147–168withpreviouslyknownalgebraicformalizationsofparallelandconcurrentpro-cesses.Modelsoflinearlogicactuallybasedo
8、nconcurrentprocesseswerealsostudied,notablybyAbramskyinthecontextofCCS[1,3]
