The need for formal methods for certifying the good behaviour of computer software is dramatically increasing with the growing complexity of the latter. Moreover, in the global computing framework one must face the additional issues of concurrency and mobility. In the recent years many new process algebras have been introduced in order to reason formally about these problems; the common pattern is to specify a type system which allows one to discriminate between *good" and "bad" processes. In this paper we focus on an incremental type system for a variation of the Ambient Calculus called M 3, i.e., Mobility types for Mobile processes in Mobile ambients and we formally prove its soundness in the proof assistant Coq. © Springer-Verlag 2004.
CITATION STYLE
Honsell, F., & Scagnetto, I. (2004). Mobility Types in Coq. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3085, 324–337. https://doi.org/10.1007/978-3-540-24849-1_21
Mendeley helps you to discover research relevant for your work.