article

Slot games: a quantitative model of computation

Author:

Dan R. GhicaAuthors Info & Claims

ACM SIGPLAN Notices, Volume 40, Issue 1

Pages 85 - 97

https://doi.org/10.1145/1047659.1040313

Published: 12 January 2005 Publication History

Abstract

We present a games-based denotational semantics for a quantitative analysis of programming languages. We define a Hyland-Ong-style games framework called slot games, which consists of HO games augmented with a new action called token. We develop a slot-game model for the language Idealised Concurrent Algol by instrumenting the strategies in its HO game model with token actions. We show that the slot-game model is a denotational semantics induced by a notion of observation formalised in the operational theory of improvement of Sands, and we give a full abstraction result. A quantitative analysis of programs has many potential applications, from compiler optimisations to resource-constrained execution and static performance profiling. We illustrate several such applications with putative examples that would be nevertheless difficult, if not impossible, to handle using known operational techniques.

References

[1]

Abramsky, S., Ghica, D. R., Murawski, A. S., and Ong, C.-H. L. Applying game semantics to compositional software modeling and verification. In TACAS (Barcelona, 2004), LNCS 2988.]]

[2]

Abramsky, S., Jagadeesan, R., and Malacaria, P. Full abstraction for PCF. Information and Computation 163 (2000).]]

Digital Library

[3]

Abramsky, S., and McCusker, G. Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions (extended abstract). ENTCS 3, (1996).]]

[4]

Berry, G., and Curien, P.-L. Sequential algorithms on concrete data structures. TCS 20 (1982), 265--321.]]

[5]

Bjerner, B., and Holmström, S. A compositional approach to time analysis of first order lazy functional programs. In Fourth International Conference on Functional Programming Languages and Computer Architecture (1989).]]

Digital Library

[6]

Brookes, S., and Geva, S. Computational comonads and intensional semantics. In Applications of Categories in Computer Science: Proceedings LMS Symposium (Durham, UK, 1991).]]

[7]

Ghica, D. R. Semantical analysis of specification logic, 3: An operational approach. In ESOP (Barcelona, 2004), LNCS 2986.]]

[8]

Ghica, D. R., Murawski, A., and Ong, C.-H. L. Syntactic control of concurrency. In ICALP (Turku, Finland, 2004), LNCS 3142.]]

[9]

Ghica, D. R., and Murawski, A. S. Angelic semantics of fine-grained concurrency. Tech. Rep. PRG-RR-03-20, Oxford University Computing Laboratory, 2003. http://users.ox.ac.uk/~coml0074/papers/asfgc.pdf.]]

[10]

Ghica, D. R., and Murawski, A. S. Angelic semantics of fine-grained concurrency. In FOSSACS (Barcelona, 2004), LNCS 2987.]]

[11]

Gurr, D. J. Semantic frameworks for complexity. PhD thesis, University of Edinburgh, 1991.Gurr, D. J. Semantic frameworks for complexity. PhD thesis, University of Edinburgh, 1991.]]

[12]

Gustavsson, J., and Sands, D. A foundation for space-safe transformations of call-by-need programs. In Higher Order Operational Techniques (Paris, France, 1999), ENTCS 26.]]

[13]

Hyland, J. M. E., and Ong, C.-H. L. On full abstraction for PCF: I, II and III. Information and Computation 163, 8 (Dec. 2000).]]

Digital Library

[14]

Jay, C. B., Cole, M. I., Sekanina, M., and Steckler, P. A monadic calculus for parallel costing of a functional language of arrays. LNCS 1300 (1990), 650--665.]]

[15]

Jifeng, H., Josephs, M. B., and Hoare, C. A. R. A theory of synchrony and asynchrony. In Programming Concepts and Methods. Elsevier, 1990, pp. 459--473.]]

[16]

Lacey, D., Jones, N. D., Wyk, E. V., and Frederiksen, C. C. Proving correctness of compiler optimizations by temporal logic. In 29th POPL (Portland, OR, USA, 2002).]]

Digital Library

[17]

Laird, J. A games semantics for idealized CSP. In MFPS 17 (Aarhus, Denmark, 2001), ENTCS 45.]]

[18]

Leperchey, B. Time and games. http://www.pps.jussieu.fr/~leperche/pub/time.ps.gz.]]

[19]

Mason, I. A., and Talcott, C. L. Equivalence in functional languages with effects. Journal of Functional Programming 1 (1991), 287--327.]]

[20]

Milner, R. Processes: a mathematical model of computing agents. In Logic Colloquium'73 (1975), H. E. Rose and J. C. Shepherdson, Eds., North-Holland, Amsterdam, pp. 157--174.]]

[21]

Moran, A., and Sands, D. Improvement in a lazy context: An operational theory for call-by-need. In 26th POPL (San Antonio, Texas, 1999).]]

Digital Library

[22]

Nickau, H. Hereditarily sequential functionals. LNCS 813 (1994).]]

Digital Library

[23]

O'Hearn, P., Reynolds, J., and Yang, H. Local reasoning about programs that alter data structures. In Proceedings of the Annual Conference of the European Association for Computer Science Logic (2001), LNCS 2142.]]

Digital Library

[24]

O'Hearn, P. W., and Riecke, J. G. Kripke logical relations and PCF. Information and Computation 120, 1 (July 1995), 107--116.]]

Digital Library

[25]

Pitts, A. M. Reasoning about local variables with operationally-based logical relations. In 11th LICS (1996), Washington, USA.]]

Digital Library

[26]

Plotkin, G. D. Lcf considered as a programming language. TCS 5 (1977), 223--255.]]

[27]

Reynolds, J. C. Idealized Algol and its specification logic. In Tools and Notions for Program Construction (Nice, France, 1981), D. Néel, Ed., Cambridge University Press, Cambridge, 1982.]]

[28]

Roscoe, W. A. Theory and Practice of Concurrency. Prentice-Hall, 1998.]]

Digital Library

[29]

Sands, D. Calculi for Time Analysis of Functional Programs. PhD thesis, Unversity of London, 1990.]]

[30]

Sands, D. Operational theories of improvement in functional languages (extended abstract). In Proceedings of the Fourth Glasgow Workshop on Functional Programming (Skye, August 1991), Workshops in Computing Series.]]

Digital Library

[31]

Sands, D. Improvement theory and its applications. In Higher Order Operational Techniques in Semantics, A. D. Gordon and A. M. Pitts, Eds., Publications of the Newton Institute. Cambridge University Press, 1998.]]

Digital Library

[32]

Scott, D. S. A type-theoretical alternative to Cuch, Iswim, Owhy. Privately circulated memo, Oxford University, Oct. 1969. Published in Theoretical Computer Science, 121(1/2):411--440, 1993.]]

Digital Library

[33]

van Stone, K. A denotational approach to measuring complexity in functional programs. PhD thesis, Carnegie Mellon University, 2003.]]

Digital Library

[34]

Tarski, A. Logic, Semantics, and Meta-Mathematics. Oxford University Press, Oxford, 1956.]]

[35]

Udding, J. T. A formal model for defining and classifying delay-insensitive circuits and systems. Distributed Computing 1(4) (1986), 197--204.]]

[36]

Wadler, P. Strictness analysis aids time analysis. In 15th POPL (January 1988).]]

Digital Library

Cited By

Laird JGorla D(2021)A compositional cost model for the λ-calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470567(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470567
Yamada N(2018)A game-semantic model of computationResearch in the Mathematical Sciences10.1007/s40687-018-0163-z6:1Online publication date: 12-Nov-2018
https://doi.org/10.1007/s40687-018-0163-z
Laird J(2017)From Qualitative to Quantitative SemanticsProceedings of the 20th International Conference on Foundations of Software Science and Computation Structures - Volume 1020310.1007/978-3-662-54458-7_3(36-52)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54458-7_3
Show More Cited By

Index Terms

Slot games: a quantitative model of computation
1. Computing methodologies
  1. Modeling and simulation
    1. Model development and analysis
      1. Modeling methodologies
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Denotational semantics

Recommendations

Slot games: a quantitative model of computation
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We present a games-based denotational semantics for a quantitative analysis of programming languages. We define a Hyland-Ong-style games framework called slot games, which consists of HO games augmented with a new action called token. We develop a slot-...
Modeling Security Protocols as Games
IAS '07: Proceedings of the Third International Symposium on Information Assurance and Security

We model security protocols as a game tree using concepts of game semantics. The model interprets protocol specifications as strategies over a game tree that represents the type of the protocol. The specifications are written in the simple arrow ...
Asynchronous games 2: the true concurrency of innocence
Concurrency theory (CONCUR 2004)

In game semantics, the higher-order value passing mechanisms of the λ-calculus are decomposed as sequences of atomic actions exchanged by a Player and its Opponent. Seen from this angle, game semantics is reminiscent of trace semantics in concurrency ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 40, Issue 1

Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2005

391 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1047659

Issue’s Table of Contents

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
402 pages
ISBN:158113830X
DOI:10.1145/1040305
General Chair:
Jens Palsberg
University of California, Los Angeles, CA
,
Program Chair:
Martín Abadi
University of California, Santa Cruz, CA

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2005

Published in SIGPLAN Volume 40, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
540
Total Downloads

Downloads (Last 12 months)14
Downloads (Last 6 weeks)1

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Laird JGorla D(2021)A compositional cost model for the λ-calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470567(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470567
Yamada N(2018)A game-semantic model of computationResearch in the Mathematical Sciences10.1007/s40687-018-0163-z6:1Online publication date: 12-Nov-2018
https://doi.org/10.1007/s40687-018-0163-z
Laird J(2017)From Qualitative to Quantitative SemanticsProceedings of the 20th International Conference on Foundations of Software Science and Computation Structures - Volume 1020310.1007/978-3-662-54458-7_3(36-52)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54458-7_3
Ghica DSmith A(2014)Bounded Linear Types in a Resource SemiringProceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 841010.1007/978-3-642-54833-8_18(331-350)Online publication date: 5-Apr-2014
https://dl.acm.org/doi/10.1007/978-3-642-54833-8_18
Hankin CMalacaria P(2013)Payoffs, Intensionality and Abstraction in GamesComputation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky10.1007/978-3-642-38164-5_6(69-82)Online publication date: 2013
https://doi.org/10.1007/978-3-642-38164-5_6
Accattoli BLancelot AManzonetto GVanoni G(2025)Interaction EquivalenceProceedings of the ACM on Programming Languages10.1145/37048919:POPL(1627-1656)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704891
Ghica D(2023)The Far Side of the CubeSamson Abramsky on Logic and Structure in Computer Science and Beyond10.1007/978-3-031-24117-8_6(219-250)Online publication date: 2-Aug-2023
https://doi.org/10.1007/978-3-031-24117-8_6
Laird J(2021)A Compositional Cost Model for the λ-calculus2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS52264.2021.9470567(1-13)Online publication date: 29-Jun-2021
https://doi.org/10.1109/LICS52264.2021.9470567
Hackett JHutton G(2019)Call-by-need is clairvoyant call-by-valueProceedings of the ACM on Programming Languages10.1145/33417183:ICFP(1-23)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341718
Alcolei AClairambault PLaurent O(2019)Resource-Tracking Concurrent GamesFoundations of Software Science and Computation Structures10.1007/978-3-030-17127-8_2(27-44)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1007/978-3-030-17127-8_2
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents