A short note on type-inhabitation: formula-trees vs. game semantics

DOI10.1016/J.IPL.2015.05.004zbMATH Open1332.03003OpenAlexW247023568MaRDI QIDQ2353633FDOQ2353633

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

zbMATH Keywords

game semanticslambda calculusautomatic theorem provingtype-inhabitation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Cites Work

• Title not available (Why is that?)
• A short note on type-inhabitation: formula-trees vs. game semantics
• On Long Normal Inhabitants of a Type
• 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 λ-Calculus
• Studying provability in implicational intuitionistic 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

Uses Software

• Automath

Recommendations

• Title not available (Why is that?) 👍 👎
• Linking Game-Theoretical Approaches with Constructive Type Theory 👍 👎
• Curry-style type isomorphisms and game semantics 👍 👎
• The paradox of trees in type theory 👍 👎
• Game semantics for dependent types 👍 👎
• Game Semantics for Type Soundness 👍 👎
• Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus 👍 👎
• Innocent Game Semantics via Intersection Type Assignment Systems 👍 👎
• Two-Level Game Semantics, Intersection Types, and Recursion Schemes 👍 👎
• An Extension of the Formulas-as-Types Paradigm 👍 👎

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)