5
$\begingroup$

Is there any work on mechanization of game semantics?

I have no experience in this area but game semantics are supposed to provide interesting denotational semantics for a variety of programming languages and logics.

I've played a tiny tiny bit with game semantics in Coq mostly based on plato.stanford.edu but I really don't know enough about the subject to know if I've given a faithful mechanization.

$\endgroup$
2
  • 1
    $\begingroup$ Martin Escardo and Paulo Olivia have been working on some stuff in Agda cs.bham.ac.uk/~mhe/TypeTopology/… However the associated papers aren't ready yet. $\endgroup$ Dec 1, 2022 at 20:45
  • $\begingroup$ I think Escardo&Oliva's work is actually closer to game theory than game semantics $\endgroup$ Jun 17, 2023 at 1:27

3 Answers 3

7
$\begingroup$

A student of mine has a partial formalization of game semantics for affine logic based on "A game semantics for linear logic" by Andreas Blass. The winning strategies for more complicated connectives like tensor are not yet formalized, but the basic framework is set up.

$\endgroup$
5
$\begingroup$

Maybe this answer is not quite in the spirit of your question, however the work "CryptHOL: Game-Based Proofs in Higher-Order Logic" (ref) and its implementation on AFP (ref) provide a framework for security proofs of cryptographic protocols, from its abstract:

Game-based proofs are a well-established paradigm for structuring security arguments and simplifying their understanding. We present a novel framework, CryptHOL, for rigorous game-based proofs that is supported by mechanical theorem proving. CryptHOL is based on a new semantic domain with an associated functional programming language for expressing games. We embed our framework in the Isabelle/HOL theorem prover and, using the theory of relational parametricity, we tailor Isabelle’s existing proof automation to game-based proofs. [..]

You can find a nice tutorial introduction here.


Since you mentioned Coq, there seems similar work going on in Coq: "SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq" (ref)

$\endgroup$
3
$\begingroup$

Dominik Wehr has mechanised Lorenzen's dialogue game semantics in Coq during his bachelor's project, including completeness results. A condensed exposition can be found in Section 5 of our journal paper.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.