Inhabitation of Low-Rank Intersection Types

DOI10.1007/978-3-642-02273-9_26MaRDI QIDQ3637206zbMATH OpenOpenAlexFDO

Authors Paweł Urzyczyn

Publication date 7 July 2009

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-02273-9_26

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• The Inhabitation Problem for Rank Two Intersection Types
• Inhabitation for non-idempotent intersection types
• Undecidability of intersection type inhabitation at rank 3 and its formalization
• The Inhabitation Problem for Non-idempotent Intersection Types
• The emptiness problem for intersection types

Cites work

• An extension of basic functionality theory for -calculus
• Embedding a second-order type system into an intersection type system
• scientific article; zbMATH DE number 2185668 (Why is no real title available?)
• scientific article; zbMATH DE number 176126 (Why is no real title available?)
• scientific article; zbMATH DE number 2087541 (Why is no real title available?)
• scientific article; zbMATH DE number 1841834 (Why is no real title available?)
• Intersection types and lambda models
• Intersection Types as Logical Formulae
• Intersection-types à la Church
• Lectures on the Curry-Howard isomorphism
• Principality and type inference for intersection types using expansion variables
• The ``relevance of intersection and union types
• The completeness of provable realizability
• The emptiness problem for intersection types
• The Inhabitation Problem for Rank Two Intersection Types
• Theory of computation.
• Types, potency, and idempotency: why nonlinearity and amnesia make a type system work

Cited in

(18)

• Pre-grammars and inhabitation for a subset of rank 2 intersection types
• Finite combinatory logic with intersection types
• The Inhabitation Problem for Non-idempotent Intersection Types
• The Inhabitation Problem for Rank Two Intersection Types
• Inhabitation in Intersection and Union Type Assignment Systems
• Inhabitation for non-idempotent intersection types
• The emptiness problem for intersection types
• A unifying framework for type inhabitation
• Tight typings and split bounds, fully developed
• Typability in bounded dimension
• Undecidability of intersection type inhabitation at rank 3 and its formalization
• Simple subtypes of intersection types
• Intersection type matching with subtyping
• The intersection type unification problem
• Intersection type calculi of bounded dimension
• On the Mints hierarchy in first-order intuitionistic logic
• Inhabitation of polymorphic and existential types
• Pregrammars and intersection types

This page was built for publication: Inhabitation of Low-Rank Intersection Types

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