Inspired by the analytical summaries of Olivier Danvy from his 2025 research talk at the College de France, we discuss the polymorphism of continuation return (co-domain) types. We then show how to use polymorphic continuation-ofcontinuation models to implement a normalizer for a version of Danvy and Filinski’s delimited control operator shift that does not need an explicit reset delimiter.

Turning the attention to the argument (domain) type of continuations, and applying the exp-log normalization to this type, leads to a notion of model allowing to produce syntactic normal forms that make deciding eta-equality (in presence of co-products) easier and finally to an intuitionistic arithmetical hierarchy.