a paper on call-by-value recursion

Dear colleagues,

We wonder if the following paper is of some interest to you -- in
particular to those studying semantics of ML-like typed call-by-value
programming languages (possibly with side effects like first-class


Axioms for Recursion in Call-by-Value

by Masahito Hasegawa and Yoshihiko Kakutani 

We propose an axiomatization of fixpoint operators in typed
call-by-value programming languages, and give its justifications in
two ways. First, it is shown to be sound and complete for the notion
of uniform T-fixpoint operators of Simpson and Plotkin. Second, the
axioms precisely account for Filinski's fixpoint operator derived from 
an iterator (infinite loop constructor) in the presence of first-class
continuations, provided that we define the uniformity principle on
such an iterator via a notion of effect-freeness (centrality). We then
explain how these two results are related in terms of the underlying
categorical structures. 

recursion, iteration, call-by-value, continuations, categorical semantics. 

An extended abstract (short version) has appeared in 
Proc. Foundations of Software Science and Computation Structures
(FoSSaCS2001), Springer LNCS 2030 (2001) pp.246-260.

A full version will appear in Higher-Order and Symbolic Computation.

Electronic copies of both versions, as well as further information
on this work are available from



Let us add a few more comments. This work can be read in two ways:

- (for semantics-minded readers) as a syntactic realization of Simpson
  and Plotkin's proposal (LICS2000) of using their "uniform T-fixed
  point operators" (where T is a strong monad used in the Moggi-style
  "monadic" modelling of call-by-value languages) as a semantics of 
  call-by-value recursion  

- (for syntax-minded readers) as a semantic analysis of Filinski's
  pioneering work on recursion and iteration in call-by-value 
  languages in the presence of first-class continuations (Lisp and
  Symbolic Computation, 1994) 

In fact, as described in the abstract, we offer a unified view on
these readings: the latter is obtained as an instance of the former, 
by instantiating the strong monad T to be the continuation monad.

This story was made possible by employing the ideas and results from 
the work by Power&Robinson, Thielecke, Fuhrman and Selinger on the
"direct-style" models of call-by-value programming languages. 
In particular, it turns out to be crucial to sort out the relationship
between the "effect-freeness" in call-by-value languages and the
"uniformity principle" for call-by-value recursion. To this end, we
propose the notion of "rigid functional" (which is a refinement of the
notion with the same name introduced by Filinski) as a natural notion
of "strictness" in a call-by-value setting.


Masahito and Yoshihiko.

Masahito Hasegawa <hassei@kurims.kyoto-u.ac.jp>
Yoshihiko Kakutani <kakutani@kurims.kyoto-u.ac.jp>
Research Institute for Mathematical Sciences, Kyoto University