Axioms for recursion in call-by-value (extended abstract)

Masahito Hasegawa and Yoshihiko Kakutani

In Proc. Foundations of Software Science and Computation Structures (FoSSaCS 2001), Springer LNCS 2030 (2001) 246-260


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.

© Springer-Verlag 2001

[ps file] [pdf file] [correction] [picture]

[info. on the full version (Higher-Order and Symbolic Computation)]

Pointers to Related Work

Back to Hassei's Research Page / Home Page