Hostname: page-component-cd9895bd7-7cvxr Total loading time: 0 Render date: 2024-12-22T09:09:02.106Z Has data issue: false hasContentIssue false
  • English
  • Français

Games and Definability For FPC

Published online by Cambridge University Press:  15 January 2014

Guy McCusker
Guy McCusker*
Affiliation:
St John's College, Oxford, United KingdomOX1 3JP.E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

A new games model of the language FPC, a type theory with products, sums, function spaces and recursive types, is described. A definability result is proved, showing that every finite element of the model is the interpretation of some term of the language.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 3 , Issue 3 , September 1997 , pp. 347 - 362
Copyright
Copyright © Association for Symbolic Logic 1997

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Abramsky, S., Axioms for full abstraction and full completeness, Unpublished manuscript, 1996.Google Scholar
[2] Abramsky, S. and Jagadeesan, R., Games and full completeness for multiplicative linear logic, Journal of Symbolic Logic, vol. 59 (1994), no. 2, pp. 543–574, Also appeared as Technical Report 92/24 of the Department of Computing, Imperial College of Science, Technology and Medicine.CrossRefGoogle Scholar
[3] Abramsky, S., Jagadeesan, R., and Malacaria, P., Full abstraction for PCF, Submitted for publication, 1996.Google Scholar
[4] Abramsky, S. and McCusker, G., Games and full abstraction for the lazy λ-calculus, In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science [18], pp. 234–243.Google Scholar
[5] Abramsky, S. and McCusker, G., Games for recursive types, Theory and formal methods of computing 1994: Proceedings of the Second Imperial College Department of Computing Workshop on Theory and Formal Methods (Hankin, Chris L., Mackie, Ian C., and Nagarajan, Rajagopal, editors), Imperial College Press, 10 1995.Google Scholar
[6] Abramsky, S. and McCusker, G., Call-by-value games, Submitted for publication, 1997.Google Scholar
[7] Abramsky, S. and McCusker, G., Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions, Algol-like languages (O'Hearn, Peter W. and Tennent, Robert D., editors), Birkhaüser, 1997, pp. 297–329 of volume 2.Google Scholar
[8] Blass, A., A game semantics for linear logic, Annals of Pure and Applied Logic, vol. 56 (1992).CrossRefGoogle Scholar
[9] Felscher, W., Dialogues as a foundation for intuitionistic logic, Handbook of philosophical logic, volume iii (Gabbay, D. and Guenther, F., editors), D. Reidel Publishing Company, 1986, pp. 341–372.Google Scholar
[10] Fiore, M. P., Axiomatic domain theory in categories of partial maps, Distinguished Dissertations in Computer Science, Cambridge University Press, 1996.Google Scholar
[11] Freyd, P. J., Algebraically complete categories, Proc. 1990 como category theory conference (Berlin) (Carboni, A. et al., editors), Springer-Verlag, 1991, Lecture Notes in Mathematics Vol. 1488, pp. 95–104.Google Scholar
[12] Girard, J-Y., Linear Logic, Theoretical Computer Science, vol. 50 (1987), no. 1, pp. 1–102.CrossRefGoogle Scholar
[13] Honda, K. and Yoshida, N., Game theoretic analysis of call-by-value computation, Submitted for publication, 1996.Google Scholar
[14] Hughes, D., Games and definability for System F, In Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science [20], pp. 76–86.Google Scholar
[15] Huwig, H. and Poigné, A., A note on inconsistencies caused by fixpoints in a cartesian closed category, Theoretical Computer Science, vol. 73 (1990), pp. 101–112.CrossRefGoogle Scholar
[16] Hyland, J. M. E. and Ong, C.-H.L., Fair games and full completeness for Multiplicative Linear Logic without the Mix-Rule, available from ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Luke.Ong, 1993.Google Scholar
[17] Hyland, J. M. E. and Ong, C.-H.L., On full abstraction for PCF: I, II and III, 130 pages, ftp-able at theory.doc.ic.ac.ukdirectory papers/Ong, 1994.Google Scholar
[18] IEEE Computer Society Press, Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, 1995.Google Scholar
[19] IEEE Computer Society Press, Proceedings, Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996.Google Scholar
[20] IEEE Computer Society Press, Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997.Google Scholar
[21] Laird, J., Full abstraction for functional languages with control, In Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science [20], pp. 58–67.Google Scholar
[22] Lamarche, F., Games semantics for full propositional linear logic, In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science [18], pp. 464–473.Google Scholar
[23] Lorenzen, P., Logik und Agon, Atti del congresso internazionale di filosofia (Firenze), Sansoni, 1960, pp. 187–194.Google Scholar
[24] Lorenzen, P., Ein dialogisches Konstruktivitätskriterium, Infinitistic methods (Warszawa), PWN, 1961, Proceed. Symp. Foundations of Math., pp. 193–200.Google Scholar
[25] McCusker, G., Games and full abstraction for a functional metalanguage with recursive types, Ph.D. thesis , Department of Computing, Imperial College, University of London, 1996.Google Scholar
[26] McCusker, G., Games and full abstraction for FPC, In Proceedings, Eleventh Annual IEEE Symposium on Logic in Computer Science [19], pp. 174–183.Google Scholar
[27] Nickau, H., Hereditarily sequential functionals, Proceedings of the symposium on logical foundations ofcomputer science: Logic at st. petersburg, Lecture notes in Computer Science, Springer, 1994.Google Scholar
[28] Ong, C. H. L., A semantic view of classical proofs: type-theoretic, categorical and denotational characterizations, In Proceedings, Eleventh Annual IEEE Symposium on Logic in Computer Science [19], pp. 230–241.Google Scholar
[29] Plotkin, G., LCF considered as a programming language, Theoretical Computer Science, vol. 5 (1977), pp. 223–255.Google Scholar
[30] Winskel, G., The formal semantics of programming languages, Foundations of Computing, The MIT Press, Cambridge, Massachusetts, 1993.CrossRefGoogle Scholar