### 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

### 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.
© Springer-Verlag 2001

### Pointers to Related Work

- A. Filinski,
**Recursion from iteration**.
*Lisp and Symbolic Comput.* **7**(1) (1994) 11-38.
- Y. Kakutani,
**Duality between call-by-name recursion and call-by-value iteration**.
In *Proc. Computer Science Logic*, Springer LNCS (2002) pp. 506-521.
- P.
Selinger,
**Control categories and duality: on the categorical semantics of
the lambda-mu calculus**.
*Math. Structures Comput. Sci.* **11**(2) (2001) 207-260.
- A.K. Simpson and
G.D. Plotkin,
**Complete axioms for categorical fixed-point operators**.
In *Proc. 15th Annual Symposium on Logic in Computer
Science* (2000) pp.30-41.

Back to Hassei's
Research Page / Home Page