Continuation Models for the Lambda Calculus With Constructors

Abstract : The lambda calculus with constructors decomposes the pattern matching a 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.
Document type :
Conference papers
Liste complète des métadonnées
Contributor : Davide Sangiogi <>
Submitted on : Tuesday, November 26, 2013 - 11:07:26 AM
Last modification on : Tuesday, April 24, 2018 - 1:52:32 PM


  • HAL Id : hal-00909364, version 1



Barbara Petit. Continuation Models for the Lambda Calculus With Constructors. Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII), 2012, Unknown, pp.337--350. ⟨hal-00909364⟩



Record views