A short note on type-inhabitation: formula-trees vs. game semantics
From MaRDI portal
Publication:2353633
DOI10.1016/j.ipl.2015.05.004zbMath1332.03003MaRDI QIDQ2353633
Publication date: 15 July 2015
Published in: Information Processing Letters (Search for Journal in Brave)
Full work available at URL: http://repositorio.inesctec.pt/handle/123456789/5222
Related Items
Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search, Intuitionistic games: determinacy, completeness, and normalization, A coinductive approach to proof search through typed lambda-calculi, A short note on type-inhabitation: formula-trees vs. game semantics
Uses Software
Cites Work
- Unnamed Item
- The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic
- Normal proofs and their grammar
- A short note on type-inhabitation: formula-trees vs. game semantics
- Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus
- On Long Normal Inhabitants of a Type
- Studying provability in implicational intuitionistic logic