Inhabitation for non-idempotent intersection types

DOI10.23638/LMCS-14(3:7)2018MaRDI QIDQ4580327zbMATH OpenFDO

Authors Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca

Publication date 15 August 2018

Full work available at URL https://arxiv.org/abs/1712.03829

zbMATH Keywords

lambda-calculusinhabitation problemnon-idempotent intersection typestype-assignment systems

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

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

Cites work

• scientific article; zbMATH DE number 2185668 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 1479634 (Why is no real title available?)
• scientific article; zbMATH DE number 7204443 (Why is no real title available?)
• scientific article; zbMATH DE number 6744146 (Why is no real title available?)
• A linearization of the Lambda-calculus and consequences
• A type assignment system for game semantics
• An extension of basic functionality theory for \(\lambda\)-calculus
• Bounding normalization time through intersection types
• Complete restrictions of the intersection type discipline
• Essential and relational models
• Infinitary intersection types as sequences. A new answer to Klop's problem
• Intersection type calculi of bounded dimension
• Non-idempotent intersection types and strong normalisation
• Non-idempotent intersection types for the lambda-calculus
• Not Enough Points Is Enough
• Principality and type inference for intersection types using expansion variables
• Quantitative types for the linear substitution calculus
• Reasoning about call-by-need by means of types
• Solvability in resource lambda-calculus
• The Inhabitation Problem for Non-idempotent Intersection Types
• The Inhabitation Problem for Rank Two Intersection Types
• The Logic of Persistent Intersection
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• The Scott model of linear logic is the extensional collapse of its relational model
• The emptiness problem for intersection types
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Types, potency, and idempotency: why nonlinearity and amnesia make a type system work

Cited in

(14)

• The emptiness problem for intersection types
• The Inhabitation Problem for Non-idempotent Intersection Types
• Resourceful program synthesis from graded linear types
• The Inhabitation Problem for Rank Two Intersection Types
• Simple subtypes of intersection types
• Intersection type calculi of bounded dimension
• Inhabitation of Low-Rank Intersection Types
• Inhabitation in Intersection and Union Type Assignment Systems
• Solvability = typability + inhabitation
• Loader and Urzyczyn are logically related
• Pre-grammars and inhabitation for a subset of rank 2 intersection types
• Undecidability of intersection type inhabitation at rank 3 and its formalization
• Typability in bounded dimension
• Inhabitation of polymorphic and existential types

This page was built for publication: Inhabitation for non-idempotent intersection types

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