Game Semantics for Free Cartesian Closed Categories: A Clear Account of the Correspondence with the ccc-Calculus
Ruben Zilibowitz – 26 April 2023
In this talk, I will discuss combinatorial structures used to present the game semantics for a free cartesian closed category (ccc), as outlined in my MRes thesis. Specifically, I will explain how the game semantics of a free ccc corresponds to a known representation of a free ccc called the ccc-calculus. This correspondence is achieved by introducing invertible constants into the ccc-calculus, resulting in a natural and intuitive connection between game semantics and the theory of long beta-eta normal forms. The proof technique employed in this account is relatively easy to understand and visualise, providing a clearer account of the free case compared to existing literature. Additionally, I will give a novel approach to computing long beta-eta normal forms in the context of this correspondence. If time permits, I will also touch upon potential generalisations of this work that are currently in a conjectural stage.This is the second talk I have given in this seminar about my MRes work, the first being in July 2022. Having since submitted my thesis, I would now like to give a more comprehensive description of these ideas.
Back