On Long Normal Inhabitants of a Type

DOI10.1093/logcom/exi016zbMath1086.03011OpenAlexW2036947136MaRDI QIDQ3025341

Sabine Broda, Luís Damas

Publication date: 13 July 2005

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exi016

zbMATH Keywords

natural deductionLambda calculusnormal inhabitantsnormal proofssimple types

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items

Intuitionistic games: determinacy, completeness, and normalization ⋮ Hammer for Coq: automation for dependent type theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A coinductive approach to proof search through typed lambda-calculi ⋮ Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus ⋮ On the expressive power of schemes ⋮ Unnamed Item ⋮ Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search ⋮ Pre-grammars and inhabitation for a subset of rank 2 intersection types ⋮ A short note on type-inhabitation: formula-trees vs. game semantics

This page was built for publication: On Long Normal Inhabitants of a Type