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.
Type de document :
Communication dans un congrès
Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII), 2012, Unknown, 286, pp.337--350, 2012
Liste complète des métadonnées

https://hal.inria.fr/hal-00909364
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 11:07:26
Dernière modification le : mardi 24 avril 2018 - 13:52:32

Identifiants

  • HAL Id : hal-00909364, version 1

Collections

Citation

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, 286, pp.337--350, 2012. 〈hal-00909364〉

Partager

Métriques

Consultations de la notice

99