Higher-Order and Symbolic Computation, 15(2/3)235-264
Axioms for Recursion in Call-by-ValueMasahito Hasegawa, Research Institute for Mathematical Sciences, Kyoto University, Kyoto 606-8502, Japan
Yoshihiko Kakutani, Research Institute for Mathematical Sciences, Kyoto University, Kyoto 606-8502, Japan
|
Abstract: 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.
Keywords: recursion, iteration, call-by-value, continuations, categorical semantics |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)