Semantics Club 27 10 2000

Axioms for Recursion in Call-by-Value

Masahito Hasegawa

(joint work with 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 ("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.