Polymorphic Computation Systems: Theory and Practice of Confluence with Call-by-Value Polymorphic Computation Systems: Theory and Practice of Confluence with Call-by-Value

Makoto Hamana, Tatsuya Abe, and Kentaro Kikuchi. Polymorphic Computation Systems: Theory and Practice of Confluence with Call-by-Value. Science of Computer Programming, 187(102322), 2020. DOI: 10.1016/j.scico.2019.102322

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.