Barbara Petit - Semantics of Typed Lambda-Calculus with Constructors

lmcs:1067 - Logical Methods in Computer Science, March 16, 2011, Volume 7, Issue 1 -
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
Submitted on: November 22, 2009
Keywords: Computer Science - Logic in Computer Science,F.3.2, F.4.3


Consultation statistics

This page has been seen 835 times.
This article's PDF has been downloaded 672 times.