Petit, Barbara - 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: Petit, Barbara

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.


Source : oai:arXiv.org:1009.3429
DOI : 10.2168/LMCS-7(1:2)2011
Volume: Volume 7, Issue 1
Published on: March 16, 2011
Submitted on: June 25, 2015
Keywords: Computer Science - Logic in Computer Science,F.3.2, F.4.3


Share

Browsing statistics

This page has been seen 58 times.
This article's PDF has been downloaded 32 times.