Delia Kesner ; Pierre Vial - Non-idempotent types for classical calculi in natural deduction style

lmcs:4310 - Logical Methods in Computer Science, January 14, 2020, Volume 16, Issue 1 - https://doi.org/10.23638/LMCS-16(1:3)2020
Non-idempotent types for classical calculi in natural deduction styleArticle

Authors: Delia Kesner ; Pierre Vial

    In the first part of this paper, we define two resource aware typing systems for the {\lambda}{\mu}-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments-based on decreasing measures of type derivations-to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head reduction and the maximal reduction sequences to normal-form. In the second part of this paper, the {\lambda}{\mu}-calculus is refined to a small-step calculus called {\lambda}{\mu}s, which is inspired by the substitution at a distance paradigm. The {\lambda}{\mu}s-calculus turns out to be compatible with a natural extensionof the non-idempotent interpretations of {\lambda}{\mu}, i.e., {\lambda}{\mu}s-reduction preserves and decreases typing derivations in an extended appropriate typing system. We thus derive a simple arithmetical characterization of strongly {\lambda}{\mu}s-normalizing terms by means of typing.


    Volume: Volume 16, Issue 1
    Published on: January 14, 2020
    Accepted on: September 22, 2019
    Submitted on: February 23, 2018
    Keywords: Computer Science - Logic in Computer Science

    1 Document citing this article

    Consultation statistics

    This page has been seen 1600 times.
    This article's PDF has been downloaded 360 times.