-
Univers
-
Ebooks
-
Livres audio
-
Presse
-
Podcasts
-
BD
-
Documents
-
- Cours
- Révisions
- Ressources pédagogiques
- Sciences de l’éducation
- Manuels scolaires
- Langues
- Travaux de classe
- Annales de BEP
- Etudes supérieures
- Maternelle et primaire
- Fiches de lecture
- Orientation scolaire
- Méthodologie
- Corrigés de devoir
- Annales d’examens et concours
- Annales du bac
- Annales du brevet
- Rapports de stage
La lecture à portée de main
FGUC Preliminary Version
21
pages
English
Documents
Écrit par
Dale Miller
Publié par
chaeh
Lire un extrait
Lire un extrait
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe en t'inscrivant gratuitement
Découvre YouScribe en t'inscrivant gratuitement
21
pages
English
Ebook
Lire un extrait
Lire un extrait
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
-
Univers
-
Ebooks
-
Livres audio
-
Presse
-
Podcasts
-
BD
-
Documents
-
Jeunesse
-
Littérature
-
Ressources professionnelles
-
Santé et bien-être
-
Savoirs
-
Education
-
Loisirs et hobbies
-
Art, musique et cinéma
-
Actualité et débat de société
-
Jeunesse
-
Littérature
-
Ressources professionnelles
-
Santé et bien-être
-
Savoirs
-
Education
-
Loisirs et hobbies
-
Art, musique et cinéma
-
Actualité et débat de société
-
Actualités
-
Lifestyle
-
Presse jeunesse
-
Presse professionnelle
-
Pratique
-
Presse sportive
-
Presse internationale
-
Culture & Médias
-
Action et Aventures
-
Science-fiction et Fantasy
-
Société
-
Jeunesse
-
Littérature
-
Ressources professionnelles
-
Santé et bien-être
-
Savoirs
-
Education
-
Loisirs et hobbies
-
Art, musique et cinéma
-
Actualité et débat de société
- Cours
- Révisions
- Ressources pédagogiques
- Sciences de l’éducation
- Manuels scolaires
- Langues
- Travaux de classe
- Annales de BEP
- Etudes supérieures
- Maternelle et primaire
- Fiches de lecture
- Orientation scolaire
- Méthodologie
- Corrigés de devoir
- Annales d’examens et concours
- Annales du bac
- Annales du brevet
- Rapports de stage
Signaler un problème
YouScribe
Le catalogue
Le service
© 2010-2024 YouScribe
