A Proof Theoretic Approach to Operational Semantics

Dale Miller

Description

Niveau: Supérieur, Doctorat, Bac+8
APC 2005 A Proof Theoretic Approach to Operational Semantics Dale Miller 1,2 INRIA & LIX, Ecole Polytechnique Palaiseau, France Abstract Proof theory can be applied to the problem of specifying and reasoning about the operational semantics of process calculi. We overview some recent research in which ?-tree syntax is used to encode expressions containing bindings and sequent calcu- lus is used to reason about operational semantics. There are various benefits of this proof theoretic approach for the pi-calculus: the treatment of bindings can be captured with no side conditions; bisimulation has a simple and natural specifi- cation in which the difference between bound input and bound output is charac- terized using difference quantifiers; various modal logics for mobility can be spec- ified declaratively; and simple logic programming-like deduction involving subsets of second-order unification provides immediate implementations of symbolic bisim- ulation. These benefits should extend to other process calculi as well. As partial evidence of this, a simple ?-tree syntax extension to the tyft/tyxt rule format for name-binding and name-passing is possible that allows one to conclude that (open) bisimilarity is a congruence. Key words: operational semantics, proof theoretic specifications, ?-tree syntax, rule formats, pi-calculus A number of frameworks have been used to formalize the semantics of process calculi and, more generally, programming languages.

• specification using


• step transition


• schema variables


• order logic


• continuation while bound


• variable never


• proof theoretic approach


• semantics into


• theory can

Sujets

• Miller
• École polytechnique

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 20
• Langue: English

Extrait

APC 2005

A Proof Theoretic Approach to Operational Semantics

1,2 Dale Miller  INRIA & LIX, Ecole Polytechnique Palaiseau, France

Abstract Proof theory can be applied to the problem of specifying and reasoning about the operational semantics of process calculi.We overview some recent research in which -tree syntax is used to encode expressions containing bindings and sequent calcu- lus is used to reason about operational semantics.There are various benets of this proof theoretic approach for the-calculus: thetreatment of bindings can be captured with no side conditions; bisimulation has a simple and natural speci- cation in which the dierence between bound input and bound output is charac- terized using dierence quantiers; various modal logics for mobility can be spec- ied declaratively; and simple logic programming-like deduction involving subsets of second-order unication provides immediate implementations of symbolic bisim- ulation. Thesebenets should extend to other process calculi as well.As partial evidence of this, a simple-tree syntax extension to the tyft/tyxt rule format for name-binding and name-passing is possible that allows one to conclude that (open) bisimilarity is a congruence. Key words:operational semantics, proof theoretic specications, -tree syntax, rule formats,-calculus

A number of frameworks have been used to formalize the semantics of process calculi and, more generally, programming languages.For example, algebra, category theory, and I/O automata have been used to provide for- mal settings for not only specifying but also reasoning about the operational semantics of calculi and languages.In this note, we overview recent results in making use ofproof theoryto encode and reason about such operational semantics. Bythe term “proof theory” we refer the study of proofs for logics, particularly in the style initiated by Gentzen.

1 SupportforthisworkcomesfromINRIAthroughthe“EquipesAssociees”Slimmerand from the ACI grants GEOCAL and Rossignol. 2 Email:[e-mail] This paper is electronically published in Electronic Notes in Theoretical Computer Science URL:www.elsevier.nl/locate/entcs