Inhabitation for Non-idempotent Intersection Types

The inhabitation problem for intersection types in the lambda-calculus is known to be undecidable. We study the problem in the case of non-idempotent intersection, considering several type assignment systems, which characterize the solvable or the strongly normalizing lambda-terms. We prove the deci...

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2018-08, Vol.14, Issue 3
Main Authors: Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca
Format: Article
Language:English
Subjects:
computer science - logic in computer science
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The inhabitation problem for intersection types in the lambda-calculus is known to be undecidable. We study the problem in the case of non-idempotent intersection, considering several type assignment systems, which characterize the solvable or the strongly normalizing lambda-terms. We prove the decidability of the inhabitation problem for all the systems considered, by providing sound and complete inhabitation algorithms for them.
ISSN:1860-5974
DOI:10.23638/LMCS-14(3:7)2018