On Long Normal Inhabitants of a Type

DOI10.1093/LOGCOM/EXI016MaRDI QIDQ3025341zbMATH OpenOpenAlexFDO

Authors 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)

Cited in

(11)

• A unifying framework for type inhabitation
• A short note on type-inhabitation: formula-trees vs. game semantics
• Game semantics and uniqueness of type inhabitance in the simply-typed \(\lambda \)-calculus
• Pre-grammars and inhabitation for a subset of rank 2 intersection types
• On the expressive power of schemes
• scientific article; zbMATH DE number 7204434 (Why is no real title available?)
• Intuitionistic games: determinacy, completeness, and normalization
• Lower end of the linial-post spectrum
• Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
• A coinductive approach to proof search through typed lambda-calculi
• Hammer for Coq: automation for dependent type theory

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3025341)