Abstract:
We study recursion in call-by-value functional languages, and more specifically a recursion construct recently introduced by Dreyer, which builds recursive boxed values. We design a type and effect system, featuring binary effects, for a call-by-value lambda-calculus extended with this recursion construct. We show that this system has the good properties required for an implicitly, statically typed language: the typable expressions do not yield run-time errors, and a principal type can be computed for any typable expression.

[PostScript, .ps.gz]