Furio Honsell and Ivan Scagnetto
Mobility
types in Coq
Technical report, Dipartimento di Matematica e Informatica,
Università di Udine, Italy, June 2003
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 M3, i.e., Mobility types for Mobile
processes in Mobile ambients and we formally prove its soundness in
the proof assistant Coq.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43