Layered and Object-Based Game Semantics
summary
Presents a concrete game-semantics model where a layer interface is an object type plus an object strategy, implementations are regular maps from underlay to overlay, and certification means the composition of underlay strategy with the implementation map equals the overlay strategy. Demonstrates a bounded queue implemented by a ring buffer with two counters, gives an extension for nondeterministic interface sets, and models concurrency via a concurrent object space to express protected shared objects and a ticket lock; compiles down through CompCert O to C with an automatic refinement proof.
AI-written summary · about
chapters (21)
- 0:00Intro
- 0:37Certification
- 1:57Modeling State
- 2:27ObjectBased Semantics
- 3:05Object Functions
- 4:33Outline
- 4:58Signature
- 5:34StateBased Semantics
- 8:33Implementations
- 8:43Interactions
- 9:08Replay
- 9:59Overlay
- 11:13Statelessness
- 12:10Formalism
- 12:36Interfaces
- 12:48Observable Behaviors
- 14:57Certification Requirements
- 15:49Certified
- 16:27Model
- 18:00Sketch
- 19:34Questions
related talks
54mLayering: The Architecture of Programs
40mFormal semantics for multi-language programs
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
59mKEYNOTE: The Shape of a Program
37mClassical Processes in modern dress
20mMessage-Observing Sessions
35mAll the Binaries Together: A Semantic Approach to Application Binary Interfaces
32mMagical Layers - The Layered Entity Concept