The emptiness problem for intersection types

DOI10.2307/2586625zbMath0937.03022OpenAlexW2098607593MaRDI QIDQ4934035

Paweł Urzyczyn

Publication date: 17 January 2000

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2586625

zbMATH Keywords

provabilitylambda calculusemptiness problemintersection type assignmentlogic of strong conjunction

Mathematics Subject Classification ID

Undecidability and degrees of sets of sentences (03D35) Combinatory logic and lambda calculus (03B40)

Related Items (15)

A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization ⋮ Unnamed Item ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Unnamed Item ⋮ Tight typings and split bounds, fully developed ⋮ Finite Combinatory Logic with Intersection Types ⋮ Strong normalization through intersection types and memory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Inhabitation of Low-Rank Intersection Types ⋮ Recognizability in the Simply Typed Lambda-Calculus ⋮ Pre-grammars and inhabitation for a subset of rank 2 intersection types ⋮ Typability and type checking in System F are equivalent and undecidable ⋮ Essential and relational models

Cites Work

• Unnamed Item
• Unnamed Item
• The completeness of provable realizability
• An extension of basic functionality theory for \(\lambda\)-calculus
• Semantical investigations in Heyting's intuitionistic logic
• A theory of type polymorphism in programming
• Intuitionistic propositional logic is polynomial-space complete
• A filter lambda model and the completeness of type assignment
• Functional Characters of Solvable Terms
• Intersection Types as Logical Formulae

This page was built for publication: The emptiness problem for intersection types