We present a new framework of polymorphic computation rules that can accommodate a distinction between values and non-values. It is suitable for analysing fundamental calculi of programming languages. We develop a type inference algorithm and new criteria to check the confluence property. These techniques are then implemented in our automated confluence checking tool PolySOL. Its effectiveness is demonstrated through examination of various calculi, including the call-by-need lambda-calculus, Moggi's computational lambda-calculus, and skew-monoidal categories.
- Second-order algebraic theory
- Type inference
ASJC Scopus subject areas