Full abstraction for functional languages with control
- 1 December 1997
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
This paper considers the consequences of relaxing the bracketing condition on 'dialogue games', showing that this leads to a category of games which can be 'factorized' into a well-bracketed substructure, and a set of classically typed morphisms. These are shown to be sound denotations for control operators, allowing the factorization to be used to extend the definability result for PCF to one for PCF with control operators at atomic types. Thus we define a fully abstract and effectively presentable model of a functional language with non-local control as part of a modular approach to modelling non-functional features using games.Keywords
This publication has 7 references indexed in Scilit:
- A semantic view of classical proofs: type-theoretic, categorical, and denotational characterizationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A Curry-Howard foundation for functional computation with controlPublished by Association for Computing Machinery (ACM) ,1997
- Linearity, Sharing and State: a fully abstract game semantics for Idealized Algol with active expressionsElectronic Notes in Theoretical Computer Science, 1996
- A semantics of evidence for classical arithmeticThe Journal of Symbolic Logic, 1995
- Fully Abstract Semantics for Observably Sequential LanguagesInformation and Computation, 1994
- A syntactic theory of sequential controlTheoretical Computer Science, 1987
- LCF considered as a programming languageTheoretical Computer Science, 1977