Inhabitation for non-idempotent intersection types

DOI10.23638/LMCS-14(3:7)2018zbMATH Open1448.68208arXiv1712.03829MaRDI QIDQ4580327FDOQ4580327

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

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

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)

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• An extension of basic functionality theory for \(\lambda\)-calculus
• Principality and type inference for intersection types using expansion variables
• Non-idempotent intersection types and strong normalisation
• The Inhabitation Problem for Non-idempotent Intersection Types
• Solvability in resource lambda-calculus
• Not Enough Points Is Enough
• A linearization of the Lambda-calculus and consequences
• The emptiness problem for intersection types
• Bounding normalization time through intersection types
• Essential and relational models
• A type assignment system for game semantics
• Infinitary intersection types as sequences. A new answer to Klop's problem
• Title not available (Why is that?)
• Complete restrictions of the intersection type discipline
• 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
• Quantitative types for the linear substitution calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Types, potency, and idempotency: why nonlinearity and amnesia make a type system work
• Reasoning about call-by-need by means of types
• Non-idempotent intersection types for the lambda-calculus
• Title not available (Why is that?)
• Intersection type calculi of bounded dimension
• The Inhabitation Problem for Rank Two Intersection Types
• Title not available (Why is that?)
• The Logic of Persistent Intersection

Cited In (14)

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

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)