Axioms for recursion in call-by-value

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 controls, provided that we define the uniformity principle on such an iterator via a notion of effect-freeness (centrality). We also investigate how these two results are related in terms of the underlying categorical models.