 |
 |
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)2011Semantics of Typed Lambda-Calculus with ConstructorsArticle
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: arXiv.org:1009.3429
Volume: Volume 7, Issue 1
Published on: March 16, 2011
Imported on: November 22, 2009
Keywords: Computer Science - Logic in Computer Science,F.3.2, F.4.3
Classifications
Mathematics Subject Classification 20201
- 03B47 - Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
- 03B60 - Other nonclassical logic
- 03B70 - Logic in computer science
- 68Q10 - Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
- 91A80 - Applications of game theory
4 Documents citing this article
Consultation statistics
This page has been seen 2456 times.
This article's PDF has been downloaded 1057 times.