Mismatch must be treated Intuitionistically for Bisimilarity Congruences
31/3/2018: A paper on mismatch has been accepted at LICS 2018. A mismatch guard for a process is an inequality, say [x ≠ y]ok. Classically, this process is equivalent to ok, since x and y are assumed to be ground constants that cannot be instantiated to the be same. However, in the open setting, we assume x and y are variables that can be assigned any value, hence it is possible that x and y are assigned the same value, say x, at which point [x ≠ x]ok clearly cannot perform action ok, since x ≠ x can never be satisfied. Since processes [x ≠ y]ok and ok behave differently under certain assignments to variables, they should be distinguished. By treating mismatch intuitionistically, as "x = y implies false" in a suitable intuitionistic logic, we can reason symbolically with respect to all possible assignments of values to variables.