A Congruence Format for Name-passing CalculiReportar como inadecuado




A Congruence Format for Name-passing Calculi - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 COMETE - Concurrency, Mobility and Transactions LIX - Laboratoire d-informatique de l-École polytechnique Palaiseau, Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161 2 PARSIFAL - Proof search and reasoning with logic specifications LIX - Laboratoire d-informatique de l-École polytechnique Palaiseau, Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161

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.





Autor: Axelle Ziegler - Dale Miller - Catuscia Palamidessi -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados