A short note on type-inhabitation: formula-trees vs. game semantics
From MaRDI portal
Publication:2353633
DOI10.1016/J.IPL.2015.05.004zbMATH Open1332.03003OpenAlexW247023568MaRDI QIDQ2353633FDOQ2353633
Authors: Yanyan Li 
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
Recommendations
- Game semantics and uniqueness of type inhabitance in the simply-typed \(\lambda \)-calculus
- Curry-style type isomorphisms and game semantics
- Two-Level Game Semantics, Intersection Types, and Recursion Schemes
- Game semantics for type soundness
- Linking game-theoretical approaches with constructive type theory. Dialogical strategies, CTT demonstrations and the axiom of choice
- scientific article; zbMATH DE number 2185726
- An Extension of the Formulas-as-Types Paradigm
- Innocent game semantics via intersection type assignment systems
- Game semantics for dependent types
- The paradox of trees in type theory
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Cites Work
- A short note on type-inhabitation: formula-trees vs. game semantics
- On Long Normal Inhabitants of a Type
- Title not available (Why is that?)
- The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic
- Normal proofs and their grammar
- Game semantics and uniqueness of type inhabitance in the simply-typed \(\lambda \)-calculus
- Studying provability in implicational intuitionistic logic: the formula tree approach
Cited In (5)
- A short note on type-inhabitation: formula-trees vs. game semantics
- Intuitionistic games: determinacy, completeness, and normalization
- Partial proof terms in the study of idealized proof search
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
- A coinductive approach to proof search through typed lambda-calculi
Uses Software
This page was built for publication: A short note on type-inhabitation: formula-trees vs. game semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2353633)
