A Congruence Format for Name-passing Calculi

Axelle Ziegler 1 Dale Miller 2 Catuscia Palamidessi 1
1 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
2 PARSIFAL - Proof search and reasoning with logic specifications
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
Abstract : We define and use a SOS-based framework to specify the transition systems of calculi with name-passing properties. This setting uses proof-theoretic tools to take care of some of the difficulties specific to name-binding and make them easier to handle in proofs. The contribution of this paper is the presentation of a format that ensures that open bisimilarity is a congruence for calculi specified within this framework, extending the well-known tyft/tyxt format to the case of name-binding and name-passing. We apply this result to the -calculus in both its late and early semantics.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00201085
Contributor : Catuscia Palamidessi <>
Submitted on : Sunday, December 23, 2007 - 11:52:49 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Long-term archiving on: Tuesday, April 13, 2010 - 3:24:22 PM

File

report.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Axelle Ziegler, Dale Miller, Catuscia Palamidessi. A Congruence Format for Name-passing Calculi. 2nd Workshop on Structural Operational Semantics (SOS'05), Jul 2005, Lisboa, Portugal. pp.169-189, ⟨10.1016/j.entcs.2005.09.032⟩. ⟨inria-00201085⟩

Share

Metrics

Record views

627

Files downloads

241