Dynamic game semantics
From MaRDI portal
Abstract: The present paper gives a mathematical, in particular, syntax-independent, formulation of intensionality and dynamics of computation in terms of games and strategies. Specifically, we give a game semantics for a higher-order programming language that distinguishes programs with the same value yet different algorithms (or intensionality), equipped with the hiding operation on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a cartesian closed bicategory, and our game semantics forms an instance of a generalization of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be the first step towards a mathematical (both categorical and game-semantic) foundation of intensional and dynamic aspects of logic and computation; our approach should be applicable to a wide range of logics and computations.
Recommendations
Cites work
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Categorical logic and type theory
- Continuous Lattices and Domains
- Data Types as Lattices
- Full abstraction for PCF
- Geometry of interaction. V: Logic in the hyperfinite factor
- Higher-order computability
- scientific article; zbMATH DE number 439891 (Why is no real title available?)
- scientific article; zbMATH DE number 4179372 (Why is no real title available?)
- scientific article; zbMATH DE number 3889501 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 193320 (Why is no real title available?)
- scientific article; zbMATH DE number 1229489 (Why is no real title available?)
- scientific article; zbMATH DE number 1241697 (Why is no real title available?)
- scientific article; zbMATH DE number 1241700 (Why is no real title available?)
- scientific article; zbMATH DE number 1259144 (Why is no real title available?)
- scientific article; zbMATH DE number 1342245 (Why is no real title available?)
- scientific article; zbMATH DE number 555217 (Why is no real title available?)
- scientific article; zbMATH DE number 786500 (Why is no real title available?)
- scientific article; zbMATH DE number 783760 (Why is no real title available?)
- scientific article; zbMATH DE number 5038458 (Why is no real title available?)
- LCF considered as a programming language
- Lectures on the Curry-Howard isomorphism
- Linear logic
- Multiple-Bias Modelling for Analysis of Observational Data
- Notions of computation and monads
- On full abstraction for PCF: I, II and III
- Polarized games
- Processes, Terms and Cycles: Steps on the Road to Infinity
- Static Analysis
- The differential lambda-calculus
- Totality in arena games
- Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus
Cited in
(10)- A game-semantic model of computation
- Games and dynamic games
- A logic of sequentiality
- scientific article; zbMATH DE number 3926681 (Why is no real title available?)
- scientific article; zbMATH DE number 1241700 (Why is no real title available?)
- Intensionality, definability and computation
- STACS 2004
- scientific article; zbMATH DE number 7064064 (Why is no real title available?)
- A Theory for Game Theories
- Grounding game semantics in categorical algebra
This page was built for publication: Dynamic game semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4988428)
