mCRL2의 타입체킹 문제는 복잡한 서브타이핑과 함수 오버로딩, 그리고 재작성 규칙(rewrite rules) 사용으로 인해 구현이 매우 까다롭습니다.

특히, 서로 다른 오버로드 간의 타입 충돌과 모호성이 발생하며, 기존 공식 구현은 이론적 타입 시스템을 완전히 구현하지 않고 휴리스틱에 의존하고 있습니다.

저자는 안티체인(antichain) 알고리즘과 통합(unification) 기법을 적용해 타입 추론을 시도했으나, 서브타이핑과 오버로딩이 결합된 상황에서는 문제의 복잡도가 급격히 증가하여, 결국 mCRL2 타입체킹이 NP-하드 문제임을 3-SAT 문제로부터 다항 시간 내에 환원하여 증명하였습니다.

이로 인해, mCRL2의 타입체킹은 다항 시간 내에 해결할 수 없으며, 실제 구현에서는 제한된 오버로딩과 단순화된 서브타이핑 계층 도입 또는 C++ 스타일의 하향식 타입 시스템 도입이 필요하다는 결론을 제시합니다.

즉, mCRL2 타입체킹의 이론적 완전성은 현실적 제약과 복잡성으로 인해 실용적이지 않으며, 타입 시스템의 재설계가 권고됩니다.