×

zbMATH — the first resource for mathematics

Definability and full abstraction. (English) Zbl 1277.68120
Cardelli, Luca (ed.) et al., Computation, meaning, and logic. Articles dedicated to Gordon Plotkin. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 172, 301-310 (2007).
Summary: Game semantics has renewed denotational semantics. It offers, among other things, an attractive classification of programming features, and has brought a bunch of new definability results. In parallel, in the denotational semantics of proof theory, several full completeness results have been shown since the early nineties. In this note, we review the relation between definability and full abstraction, and we put a few old and recent results of this kind in perspective.
For the entire collection see [Zbl 1273.68018].

MSC:
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M.; Cardelli, L.; Curien, P.-L.; Lévy, J.-J., Explicit substitutions, Journal of functional programming, 1, 4, 375-416, (1992) · Zbl 0941.68542
[2] Abramsky, S., Domain theory in logical form, Annals of pure and applied logic, 51, 1-77, (1991) · Zbl 0737.03006
[3] Abramsky, S.; Jagadeesan, R., Games and full completeness for multiplicative linear logic, Journal of symbolic logic, 59, 2, 543-574, (1994), (conference version in Proc. FOSSACS’92) · Zbl 0822.03007
[4] Abramsky, S.; Jagadeesan, R.; Malacaria, P., Games and full abstraction for PCF, Information and computation, 163, 2, 409-470, (2000), preliminary conference version in Proc. Theoretical Aspects of Computer Science 1994, Springer LNCS 789, 1-16 · Zbl 1006.68028
[5] Abramsky, S.; McCusker, G., Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expression, () · Zbl 0909.68029
[6] Abramsky, S.; Honda, K.; McCusker, G., A fully abstract game semantics for general references, (), 334-344
[7] Amadio, R.; Curien, P.-L., Domains and lambda-calculi, (1998), Cambridge University Press · Zbl 0962.03001
[8] Berry, G., Stable models of typed lambda-calculi, () · Zbl 0382.68041
[9] Berry, G.; Curien, P.-L., Sequential algorithms on concrete data structures, Theoretical computer science, 20, 265-321, (1982) · Zbl 0497.68012
[10] Berry, G.; Curien, P.-L., The kernel of the applicative language CDS: theory and practice, (), 35-87 · Zbl 0619.68008
[11] Bucciarelli, A.; Ehrhard, T., Sequentiality in an extensional framework, Information and computation, 110, 2, 265-296, (1994) · Zbl 0807.68064
[12] Cartwright R., and M. Felleisen, Observable sequentiality and full abstraction, Proc. ACM Principles of Programming Languages 1992
[13] Cartwright, R.; Curien, P.-L.; Felleisen, M., Fully abstract semantics for observably sequential languages, Information and computation, 111, 2, 297-401, (1994) · Zbl 0806.68072
[14] Chroboczek, J., Game semantics and subtyping, in Proc. of the 15th annual IEEE symposium on Logic in Computer Science (LICS’00) · Zbl 1024.68018
[15] Coppo, M.; Dezani, M., A new type assignment for lambda-terms, Archiv. math. logik, 19, 139-156, (1978) · Zbl 0418.03010
[16] Cousineau, G.; Curien, P.-L.; Mauny, M., The categorical abstract machine, Science of computer programming, 8, 173-202, (1987) · Zbl 0634.68078
[17] Curien, P.-L., “Combinateurs catégoriques, algorithmes séquentiels et programmation fonctionnelle”, Thèse d’Etat, Univ. Paris 7 (1983)
[18] Curien, P.-L., Categorical combinators, sequential algorithms and functional programming, (1993), Birkhäuser · Zbl 0814.68085
[19] P.-L. Curien, Observable sequential algorithms on concrete data structures, Proc. 7th Symposium on Logic in Computer Science (LICS ’92), Santa Cruz, published by ACM (1992)
[20] Curien, P.-L., On the symmetry of sequentiality, (), 29-71
[21] Curien, P.-L., Sur l’η-expansion infinie, Comptes-rendus de l’académie des sciences, 334, Sec. I, 77-82, (2002) · Zbl 0996.03009
[22] Danos, V.; Harmer, R., Probabilistic game semantics, ACM transactions on computational logic, 3, 3, (2002) · Zbl 1365.68310
[23] Dimovski, A., D.R. Ghica, and R. Lazic, Data-abstraction refinement: a game semantic approach, in Proceedings of the 12th International Static Analysis Symposium (SAS’05), London (2005) · Zbl 1141.68366
[24] Ghica, D.R.; McCusker, Guy, The regular-language semantics of second-order idealized ALGOL, Theoretical computer science, 309, 1-3, 469-502, (2003) · Zbl 1070.68083
[25] Ghica, D.R.; Murawski, A., Angelic semantics of fine-grained concurrency, () · Zbl 1126.68499
[26] Girard, J.-Y., Linear logic, Theoretical computer science, 50, 1-102, (1987) · Zbl 0625.03037
[27] Girard, J.-Y., On denotational completeness, Theoretical computer science, 227, 249-273, (1999) · Zbl 0959.03050
[28] Harmer, R., and G. McCusker, A fully abstract game semantics for finite nondeterminism, in Proc. of the 14th annual IEEE symposium on Logic in Computer Science (LICS’99)
[29] Honda, K.; Yoshida, N., Game-theoretic analysis of call-by-value computation, Theoretical computer science, 221, 1-2, 393-456, (1999) · Zbl 0930.68061
[30] Hyland, J.M.E., A syntactic characterization of the equality in some models of lambda calculus, J. London math. soc., 2, 361-370, (1976) · Zbl 0329.02010
[31] Hyland, J.M.E., and C.-H.L. Ong, Fair Games and Full Completeness for Multiplicative Linear Logic without the Mix-Rule. Preprint(1993)
[32] Hyland, J.M.E.; Ong, L., On full abstraction for PCF I, II, and III, Information and computation, 163, 1, 285-408, (2000), (preliminary draft circulated since 1994) · Zbl 1006.68027
[33] Kahn, G.; Plotkin, G., Concrete domains, Theoretical computer science, 121, 187-277, (1993), (appeared in French as TR IRIA-Laboria 336 in 1978) · Zbl 0809.68085
[34] Laird, J., Full abstraction for functional languages with control, Proc. 12th Annual Symposium on Logic in Computer Science (LICS ’97) (1997)
[35] Laird, J., A fully abstract bidomain model of unary FPC, () · Zbl 1039.68034
[36] Laird, J., Games and sequential algorithms. To appear · Zbl 1351.68060
[37] Lamarche, F., Sequentiality, games and linear logic (manuscript) (1992)
[38] Loader, R., Unary PCF is decidable, Theoretical computer science, 206, 1-2, 317-329, (1998) · Zbl 0916.68017
[39] Loader, R., Finitary PCF is undecidable, Theoretical computer science, 266, 1-2, 341-364, (2001) · Zbl 0992.68017
[40] Longley, J., The sequentially realizable functionals, Annals of pure and applied logic, 117, 1-3, 1-93, (2002) · Zbl 1022.03023
[41] Malacaria, P.; Hankin, C., A new approach to control flow analysis, ()
[42] Malacaria, P.; Hankin, C., Generalised flowcharts and games, ()
[43] Malacaria, P., and C. Hankin, Non-deterministic games and program analysis: an application to security, in Proc. of the 14th annual IEEE symposium on Logic in Computer Science (LICS’99) · Zbl 1264.91034
[44] Milner, R., Fully abstract models of typed lambda-calculi, Theoretical computer science, 4, 1-23, (1977) · Zbl 0386.03006
[45] Nickau, H., Hereditarily sequential functionals, (), 253-264 · Zbl 0946.03053
[46] O’Hearn, P.; Riecke, J., Kripke logical relations and PCF, Information and computation, 120, 1, 107-116, (1995) · Zbl 0912.03008
[47] Ong, C.-H.L., Observational equivalence of third-order idealized algol is decidable, (), 245-256
[48] Paolini, L., “Lambda-theories: some investigations”, PhD thesis, Università di Genova and Université de la Méditerranée (2003)
[49] Plotkin, G., LCF as a programming language, Theoretical computer science, 5, 223-257, (1977) · Zbl 0369.68006
[50] Scott, D., A type-theoretical alternative to ISWIM, CUCH, OWHY, Theoretical computer science, 121, 411-440, (1993), (manuscript circulated since 1969) · Zbl 0942.68522
[51] Sieber, K., Reasoning about sequential functions via logical relations, () · Zbl 0798.68097
[52] Stoughton, A., Mechanizing logical relations, ()
[53] Wadsworth, C., The relation between computational and denotational properties for Scott’s D-infinity models of the lambda-calculus, SIAM journal of computing, 5, 488-521, (1976) · Zbl 0346.02013
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.