Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus

DOI10.1007/978-3-642-21691-6_8zbMath1331.03018OpenAlexW60649324MaRDI QIDQ3007657

Sylvain Salvati, Pierre Bourreau

Publication date: 17 June 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-21691-6_8

zbMATH Keywords

coherence theoremgames semanticsprincipal typingsimply-typed \(\lambda \)-calculusuniqueness of type inhabitance

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

A Datalog Recognizer for Almost Affine λ-CFGs ⋮ A coinductive approach to proof search through typed lambda-calculi ⋮ Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search ⋮ A short note on type-inhabitation: formula-trees vs. game semantics

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• On the membership problem for non-linear abstract categorial grammars
• Closed categories and the theory of proofs
• A coherence theorem for canonical morphisms in Cartesian closed categories
• A game semantics for linear logic
• Uniqueness of normal proofs in implicational intuitionistic logic
• On full abstraction for PCF: I, II and III
• On Long Normal Inhabitants of a Type
• The virtues of eta-expansion
• Dialogspiele als Semantische Grundlage von Logikkalkülen
• Innocent game models of untyped \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item