A short note on type-inhabitation: Formula-trees vs. game semantics

• A correspondence between the formula-tree of a type and the arena associated to a type.
• A correspondence between proof-trees and winning strategies in a game.
• A proof of the equivalence between the formula-tree method and the method based on game semantics.

This short note compares two different methods for exploring type-inhabitation in the simply typed lambda-calculus, highlighting their similarities.