A short note on type-inhabitation: formula-trees vs. game semantics
From MaRDI portal
Publication:2353633
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
Cites work
- scientific article; zbMATH DE number 1042221 (Why is no real title available?)
- A short note on type-inhabitation: formula-trees vs. game semantics
- Game semantics and uniqueness of type inhabitance in the simply-typed \(\lambda \)-calculus
- Normal proofs and their grammar
- On Long Normal Inhabitants of a Type
- Studying provability in implicational intuitionistic logic: the formula tree approach
- The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic
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
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)
