A typed lambda-calculus with call-by-name and call-by-value iteration

ABSTRACT. We define a simply typed lambda calculus with positive recursive types in which we study the less well-known Scott encoding of data types. Scott data types have "case distinction" as a basic feature. We shed a different light on the Scott data types, by viewing the different cases as "continuations". As Scott data types do not have iteration (or recursion) built in, we add as primitives a "call-by-name iterator" and a "call-by-value iterator" with appropriate reduction rules. We show that the calculus is strongly normalizing.