We present an axiomatic theory of contexts, i.e., terms with “holes”. The set of properties of such theory fits very well with weak-HOAS encoding techniques, where binders are represented by functional constants and the treatment of bound variables (alpha-conversion and renamings) is automatically dealt with by the metalanguage. Applying this solution to the encoding of a process algebra like, e.g., the pi-calculus in Coq gives rise to a full-fledged proof editor/proof assistant. Users no longer have to worry about explicitly renaming variables to avoid name clashes. Moreover, the formal representation of processes is very close to the original object language.

These features have immediate benefits during the formalization of processes bisimilarities. For instance, we succeeded in mechanizing a substantial chapter of the theory of strong late bisimilarity, which amounts essentially to Section 2 of A calculus of mobile processes by Milner, Parrow, and Walker.

All the axioms of our theory of contexts are satisfied in a categorical model based on presheaves, and they are compatible with the (co)inductive type theory underlying the Coq system.