Sequentiality in an extensional framework

Antonio Bucciardelli
Thomas Ehrhard

Information and Computation, 110:265--296, 1994

Available as PostScript, DVI.

Abstract:

We present a cartesian closed category of dI-domains with coherence and strongly stable functions which provides a new model of PCF, where terms are interpreted by functions and where, at first order, all functions are sequential.

We show how this model can be refined in such a way that the theory it induces on the terms of PCF be strictly finer than the theory induced by the Scott model of continuous functions.

Keywords: lambda-calculus, denotational semantics, continuity, stability, sequentiality.

Comments:
ISSN: 0890-540

Authors addresses: LIENS - DMI, Ecole Normale Supérieure, 45 rue d'Ulm, 75230 Paris Cédex, France. e-mail:buccia@dmi.ens.fr
IGM, Université de Marne-la-Vallée, 2 rue de la Butte Verte, 93166 Noisy-le-Grand Cédex, France. e-mail:ehrhard@dmi.ens.fr.

[BRICS symbol] BRICS WWW home page