FGUC Preliminary Version
21
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe et accède à tout notre catalogue !
Découvre YouScribe et accède à tout notre catalogue !
21
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
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
Voir
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
Publié par
Langue
English
