Typechecking mCRL2
Summary
The article analyzes mCRL2's nonstandard type system, including subtyping and overload resolution, and explores a proposed antichain-based type inference, followed by a unification approach. It demonstrates NP-hardness of typechecking via a 3-SAT reduction and concludes with design recommendations.