×

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
PDFBibTeX XMLCite
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, (Algol-like languages (1997), Birkhauser) · Zbl 0909.68029
[6] Abramsky, S.; Honda, K.; McCusker, G., A fully abstract game semantics for general references, (Proc. Thirteenth Annual IEEE Symposium on Logic in Computer Science (1998), IEEE Computer Society Press), 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, (Proc. ICALP. Proc. ICALP, Lect. Notes in Comp. Sci., 62 (1978), Springer) · 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, (Proc. French-US Seminar on the Applications of Algebra to Language Definition and Compilation (1985), Cambridge University Press), 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; Cartwright R., and M. Felleisen, Observable sequentiality and full abstraction
[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; Chroboczek, J., Game semantics and subtyping · 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); 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), Pitman: 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); 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, (Proc. Mathematical Foundations of Programming Semantics ’93. Proc. Mathematical Foundations of Programming Semantics ’93, Lect. Notes in Comp. Sci., 802 (1994), Springer), 29-71 · Zbl 1509.68145
[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; Dimovski, A., D.R. Ghica, and R. Lazic, Data-abstraction refinement: a game semantic approach · 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, (Proc. of Foundations of Software Science and Computation Structures (FOSSACS’04). Proc. of Foundations of Software Science and Computation Structures (FOSSACS’04), Lecture note in Computer Science, 2987 (2004)) · 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; Harmer, R., and G. McCusker, A fully abstract game semantics for finite nondeterminism
[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); 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; Laird, J., Full abstraction for functional languages with control
[35] Laird, J., A Fully Abstract Bidomain Model of Unary FPC, (Proc. of the Int. Conf. on Typed Lambda-Calculi and Applications (TLCA ’03). Proc. of the Int. Conf. on Typed Lambda-Calculi and Applications (TLCA ’03), Lecture Notes in Computer Science, 2701 (2003)) · Zbl 1039.68034
[36] Laird, J., Games and sequential algorithms; Laird, J., Games and sequential algorithms · Zbl 1351.68060
[37] Lamarche, F., Sequentiality, games and linear logic; Lamarche, F., Sequentiality, games and linear logic
[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, (Proc. of Compiler Construction 1998. Proc. of Compiler Construction 1998, Lecture Notes in Computer Science, 1383 (1998))
[42] Malacaria, P.; Hankin, C., Generalised flowcharts and games, (Proc. ICALP’98. Proc. ICALP’98, Lecture Notes in Computer Science, 1443 (1998))
[43] Malacaria, P., and C. Hankin, Non-deterministic games and program analysis: an application to security; Malacaria, P., and C. Hankin, Non-deterministic games and program analysis: an application to security · 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, (Nerode, A.; Matiyasevich, Yu. V., Proc. Logical Foundations of Computer Science: Logic at St. Petersburg. Proc. Logical Foundations of Computer Science: Logic at St. Petersburg, Lecture Notes in Computer Science, 813 (1994)), 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, (Proceedings of IEEE Symposium on Logic in Computer Science 2002, Copenhagen Denmark (2002), Computer Society Press), 245-256
[48] Paolini, L., “Lambda-theories: some investigations”, PhD thesis, Università di Genova and Université de la Méditerranée (2003); 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, (Proc. Applications of Categories in Computer Science (1992), Cambridge University Press) · Zbl 0798.68097
[52] Stoughton, A., Mechanizing logical relations, (Proc. Mathematical Foundations of Progamming Semantics. Proc. Mathematical Foundations of Progamming Semantics, Lect. Notes in Comp. Sci., 802 (1994), Springer) · Zbl 1509.68045
[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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.