Formalising a Value-Passing Calculus in HOL |
| |
| Authors: | Monica Nesi |
| |
| Affiliation: | (1) Dipartimento di Matematica Pura ed Applicata, Università degli Studi di L'Aquila, L'Aquila, Italy, IT |
| |
| 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.
Received September 1997 / Accepted in revised form July 1999 |
| |
| Keywords: | : Process calculi Higher order logic Theorem proving Meta-theoretic reasoning Formal verification |
| 本文献已被 SpringerLink 等数据库收录！ |
|
