Continuation Models for the Lambda Calculus With Constructors

The lambda calculus with constructors decomposes the pattern matching à la ML into some atomic rules. Some of them do not match with the usual computational intuitions (in particular with typing intuitions). However it is possible to define an abstract notion of model for the untyped calculus, that has a trivial syntactic instance.Nevertheless, the question of devising a non-syntactic model for this calculus was still unresolved. In this paper we answer this question in the untyped setting, by going back to the first motivation of the lambda-calculus with constructors: the simulation of an abstract machine with two independent stacks. This provides immediately a CPS translation into the usual lambda calculus. At the semantic level, it appears that this translation transforms any continuation model of the untyped lambda calculus into a model of the lambda calculus with constructors. In particular, any Scott domain can be turned into such a model.