Formalising a Value-Passing Calculus in HOL
Monica Nesi · Formal Aspects of Computing · 1999
Abstract. Milner's value-passing calculus for describing and reasoning about communicating systems is formalised in the HOL proof assistant. Based on a previously defined mechanisation of pure CCS (no data communication, only synchronisation) in HOL, value-passing agents are given behavioural semantics by translating them into pure agents. An interactive proof environment is derived that supports both reasoning about the value-passing calculus and verification of value-passing specifications, which are defined over an infinite value domain.