On Long Normal Inhabitants of a Type

DOI10.1093/LOGCOM/EXI016zbMATH Open1086.03011OpenAlexW2036947136MaRDI QIDQ3025341FDOQ3025341

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
• Title not available (Why is that?)
• 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)