Semantics Club 27 10 2000
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 ("Recursion from
Iteration"), 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 models (based on Selinger's recent work).
An extended abstract of this work is available from
here.