Technical Report:DCC-2014-08

Type-Inhabitation: Formula-Trees vs. Game Semantics

Sandra Alves,

Sabine Broda

LIACC & CMUP& DCC-FC Universidade do Porto
December 2014


Type-inhabitation is a topic of major importance, due to its close relationship to provability in logical systems and has been studied from different perspectives over the years. In 2000 a new proof method has been presented, evidencing the close relationship between the structure of types and their inhabitants. More recently, in 2011, another method has been given in the context of game semantics. In this paper we clarify the similarities between the two approaches.