Semantics of Typed Lambda-Calculus with Constructors

TL;DR

This paper introduces a typed lambda-calculus with constructors and pattern matching, proving strong normalization and match failure absence for a restricted system using reducibility techniques.

Contribution

It extends lambda-calculus with union, intersection types, and pattern matching for variadic constructors, providing formal proofs of normalization and safety.

Findings

Proved strong normalization for the restricted system.

Established absence of match failure in the system.

Extended lambda-calculus with advanced type features and constructors.

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.