We present a formalisation, in the theorem proving system Isabelle/HOL, of a linear type system for the pi calculus, including a proof of runtime safety of typed processes. The use of a uniform encoding of pi calculus syntax in a meta language, the development of a general theory of type environments, and the structured formalisation of the main proofs, facilitate the adaptation of the Isabelle theories and proof scripts to variations on the language and other type systems.
CITATION STYLE
Gay, S. J. (2001). A framework for the formalisation of pi calculus type systems in isabelle/HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2152, pp. 217–232). Springer Verlag. https://doi.org/10.1007/3-540-44755-5_16
Mendeley helps you to discover research relevant for your work.