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

DOI10.1007/978-3-642-21691-6_8zbMath1331.03018MaRDI 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 theorem; games semantics; principal typing; simply-typed \(\lambda \)-calculus; uniqueness of type inhabitance

Mathematics Subject Classification ID

03B40: Combinatory logic and lambda calculus

Related Items

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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