Polymorphic computation systems: Theory and practice of confluence with call-by-value

Makoto Hamana, Tatsuya Abe, Kentaro Kikuchi

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)


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.

Original languageEnglish
Article number102322
JournalScience of Computer Programming
Publication statusPublished - 2020 Feb 15


  • Confluence
  • Polymorphism
  • Second-order algebraic theory
  • Type inference
  • λ-calculus

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Polymorphic computation systems: Theory and practice of confluence with call-by-value'. Together they form a unique fingerprint.

Cite this