Abstract:This paper mainly studies the axiomatization of higher-order process calculi with the mismatch operator. Firstly, it formulates the theory of open weak higher-order bisimulation, and shows important properties such as equivalence and congruence. Secondly, following the method on linearity, it builds up an axiom system for finite processes. Finally, based on the characterization of open weak higher-order bisimulation, it proves the completeness of the axiom system. The work of this paper provides the basis for designing and implementing an effective algorithm for checking the bisimulation equivalence of higher-order processes with the mismatch operator, and a theoretical reference for relevant applications of modeling with higher-order processes.