2 citations · 5 across the 5 of their papers we have counts for
6 papers
Unique Solutions of Contractions, CCS, and their HOL Formalisation
Chun Tian, Davide Sangiorgi
The unique solution of contractions is a proof technique for bisimilarity that overcomes certain syntactic constraints of Milner's "unique solution of equations" technique. The pap…
A Formalization of Unique Solutions of Equations in Process Algebra
Chun Tian
In this thesis, a comprehensive formalization of Milner's Calculus of Communicating Systems (also known as CCS) has been done in HOL theorem prover (HOL4), based on an old work in…
Further Formalization of the Process Algebra CCS in HOL4
Chun Tian
In this project, we have extended previous work on the formalization of the process algebra CCS in HOL4. We have added full supports on weak bisimulation equivalence and observatio…
A Formalization of the Process Algebra CCS in HOL4
Chun Tian
An old formalization of the Process Algebra CCS (no value passing, with explicit relabeling operator) on has been ported from HOL88 theorem prover to HOL4 (Kananaskis-11 and later)…
SNMP for Common Lisp
Chun Tian
Simple Network Management Protocol (SNMP) is widely used for management of Internet-based network today. In Lisp community, there're large Lisp-based applications which may need be…
Formalized Lambek Calculus in Higher Order Logic (HOL4)
Chun Tian
In this project, a rather complete proof-theoretical formalization of Lambek Calculus (non-associative with arbitrary extensions) has been ported from Coq proof assistent to HOL4 t…