Semantics of Typed Lambda-Calculus with Constructors
Logic in Computer Science
2019-03-14 v3
Abstract
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.
Keywords
Cite
@article{arxiv.1009.3429,
title = {Semantics of Typed Lambda-Calculus with Constructors},
author = {Barbara Petit},
journal= {arXiv preprint arXiv:1009.3429},
year = {2019}
}