Antonio Bucciarelli ; Delia Kesner ; Simona Ronchi Della Rocca - Inhabitation for Non-idempotent Intersection Types

lmcs:4139 - Logical Methods in Computer Science, August 3, 2018, Volume 14, Issue 3 - https://doi.org/10.23638/LMCS-14(3:7)2018
Inhabitation for Non-idempotent Intersection TypesArticle

Authors: Antonio Bucciarelli ; Delia Kesner ; Simona Ronchi Della Rocca

    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.


    Volume: Volume 14, Issue 3
    Published on: August 3, 2018
    Accepted on: June 27, 2018
    Submitted on: December 12, 2017
    Keywords: Computer Science - Logic in Computer Science

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1860 times.
    This article's PDF has been downloaded 315 times.