| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 428856 | Information Processing Letters | 2015 | 4 Pages |
Abstract
•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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
S. Alves, S. Broda,