The emptiness problem for intersection types

DOI10.2307/2586625MaRDI QIDQ4934035zbMATH OpenOpenAlexFDO

Authors 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

emptiness problemintersection type assignmentlambda calculuslogic of strong conjunctionprovability

Mathematics Subject Classification ID

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

Recommendations

• Inhabitation for non-idempotent intersection types
• Inhabitation of Low-Rank Intersection Types
• The Inhabitation Problem for Non-idempotent Intersection Types
• scientific article; zbMATH DE number 2185668
• Inhabitation in Intersection and Union Type Assignment Systems

Cites work

• A filter lambda model and the completeness of type assignment
• A theory of type polymorphism in programming
• An extension of basic functionality theory for -calculus
• Functional Characters of Solvable Terms
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 47007 (Why is no real title available?)
• Intersection Types as Logical Formulae
• Intuitionistic propositional logic is polynomial-space complete
• Semantical investigations in Heyting's intuitionistic logic
• The completeness of provable realizability

Cited in

(27)

• Typability and type checking in System F are equivalent and undecidable
• Strong normalization through intersection types and memory
• Pre-grammars and inhabitation for a subset of rank 2 intersection types
• A type assignment for -calculus complete both for FPTIME and strong normalization
• Finite combinatory logic with intersection types
• The Inhabitation Problem for Non-idempotent Intersection Types
• Inhabitation of Low-Rank Intersection Types
• Recognizability in the Simply Typed Lambda-Calculus
• scientific article; zbMATH DE number 1479641 (Why is no real title available?)
• A resource aware semantics for a focused intuitionistic calculus
• Inhabitation for non-idempotent intersection types
• On sets of terms having a given intersection type
• The -calculus: syntax and types
• scientific article; zbMATH DE number 7204443 (Why is no real title available?)
• Tight typings and split bounds, fully developed
• Non-idempotent types for classical calculi in natural deduction style
• Undecidability of intersection type inhabitation at rank 3 and its formalization
• Decidability of several concepts of finiteness for simple types
• Simple subtypes of intersection types
• Essential and relational models
• Intersection type matching with subtyping
• The algebraic intersection type unification problem
• The intersection type unification problem
• Checking Emptiness of Non-Deterministic Regular Types with Set Operators
• Solvability = typability + inhabitation
• Pregrammars and intersection types
• Meaningfulness and genericity in a subsuming framework (invited talk)

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

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