21 pages
English

# FGUC Preliminary Version

-

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
21 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Niveau: Supérieur
FGUC 2004 Preliminary Version A Proof Search Specification of the pi-Calculus Alwen Tiu 1,3 INRIA-Futurs and Ecole polytechnique Dale Miller 2 INRIA-Futurs and Ecole polytechnique Abstract We present a meta-logic that contains a new quantifier ? (for encoding “generic judgments”) and inference rules for reasoning within fixed points of a given speci- fication. We then specify the operational semantics and bisimulation relations for the finite pi-calculus within this meta-logic. Since we restrict to the finite case, the ability of the meta-logic to reason within fixed points becomes a powerful and complete tool since simple proof search can compute this one fixed point. The ? quantifier helps with the delicate issues surrounding the scope of variables within pi- calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no side conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation. Key words: pi-calculus, names, meta-logic, proof search, bisimulation. 1 Introduction In order to treat abstractions within expressions and computation declara- tively, we shall work within a meta-logic which contains a well understood notion of abstraction: in particular, we shall work with a logic inspired by Church's Simple Theory

• pi calculus

• logic

• free variable

• empty

• differences between

• signature

• open bisimulation

• fo?∆?

• free names

Sujets

##### Signature

Informations

 Publié par chaeh Nombre de lectures 9 Langue English

Exrait

FGUC2004PreliminaryVersionAProofSearchSpeciﬁcationoftheπ-CalculusAlwenTiu1,3INRIA-FutursandE´colepolytechniqueDaleMiller2INRIA-FutursandE´colepolytechniqueAbstractWepresentameta-logicthatcontainsanewquantiﬁerr(forencoding“genericjudgments”)andinferencerulesforreasoningwithinﬁxedpointsofagivenspeci-ﬁcation.Wethenspecifytheoperationalsemanticsandbisimulationrelationsfortheﬁniteπ-calculuswithinthismeta-logic.Sincewerestricttothenitecase,theabilityofthemeta-logictoreasonwithinﬁxedpointsbecomesapowerfulandcompletetoolsincesimpleproofsearchcancomputethisoneﬁxedpoint.Therquantiﬁerhelpswiththedelicateissuessurroundingthescopeofvariableswithinπ-calculusexpressionsandtheirexecutions(proofs).Weshallillustrateseveralmeritsofthelogicalspeciﬁcationswewrite:theyarenaturalanddeclarative;theycontainnosideconditionsconcerningnamesofvariableswhilemaintainingacompletelyformaltreatmentofsuchvariables;diﬀerencesbetweenlateandopenbisimulationrelationsareeasytoseedeclaratively;andproofsearchinvolvingtheapplicationofinferencerules,uniﬁcation,andbacktrackingcanprovidecompleteproofsystemsforbothone-steptransitionsandforbisimulation.Keywords:π-calculus,names,meta-logic,proofsearch,bisimulation.1IntroductionInordertotreatabstractionswithinexpressionsandcomputationdeclara-tively,weshallworkwithinameta-logicwhichcontainsawellunderstoodnotionofabstraction:inparticular,weshallworkwithalogicinspiredbyChurch’sSimpleTheoryofTypes[4],wheretermsareactuallysimplytyped1Email:tiu@lix.polytechnique.fr2Email:dale.miller@inria.fr3ThisworkwaspartlydonewhentheauthorwasastudentatPennsylvaniaStateUniver-.ytisThisisapreliminaryversion.TheﬁnalversionwillbepublishedinElectronicNotesinTheoreticalComputerScienceURL:www.elsevier.nl/locate/entcs