Type-Inhabitation: Formula-Trees vs. Game Semantics
Sandra Alves, |
Sabine Broda |
LIACC & CMUP& DCC-FC |
Universidade do Porto |
Portugal
December 2014
Abstract
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.