Barbara Petit - Semantics of Typed Lambda-Calculus with Constructors

lmcs:1067 - Logical Methods in Computer Science, March 16, 2011, Volume 7, Issue 1 - https://doi.org/10.2168/LMCS-7(1:2)2011
Semantics of Typed Lambda-Calculus with Constructors

Authors: Barbara Petit

    We present a Curry-style second-order type system with union and intersection types for the lambda-calculus with constructors of Arbiser, Miquel and Rios, an extension of lambda-calculus with a pattern matching mechanism for variadic constructors. We then prove the strong normalisation and the absence of match failure for a restriction of this system, by adapting the standard reducibility method.


    Volume: Volume 7, Issue 1
    Published on: March 16, 2011
    Accepted on: June 25, 2015
    Submitted on: November 22, 2009
    Keywords: Computer Science - Logic in Computer Science,F.3.2, F.4.3

    4 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 1084 times.
    This article's PDF has been downloaded 833 times.