 Taking inspiration in Martin-Löf’s CTT goes with adopting an enriched language which aims at making everything explicit within the language itself. For example, quantification is always restricted to a particular specified set, so that the formula \((\forall x: A)Px\ [A: set]\) reads For all \(x\) in \(A\) \(Px\), where \(A\) is a set. Expressions such as \(A: set\) are added to the elementary statements. Importantly, this does not mean that set-theoretic semantics is suddenly introduced in the framework: CTT is in fact based on the proposition-as-type principle or Curry-Howard correspondence (see the entry on Intuitionistic Type Theory). Other works about the relation between game-based approaches to logic and Martin-Löf’s CTT have been made with different perspectives and aims, starting with Ranta (1994). Recent works have provided important results on the use of game-based approaches to CTT for constructive mathematics, inspired by Coquand (1995); see for instance Sterling (2021).