Axioms for recursion in call-by-value

Masahito Hasegawa and Yoshihiko Kakutani

Higher-Order and Symbolic Computation 15(2/3):235-264, September 2002


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.

[gzipped ps file] [pdf file] (last revision October 2001)

[info. on the conference version (FoSSaCS2001)]

Pointers to Related Work

Back to Hassei's Research Page / Home Page