Semantics of Typed Lambda-Calculus with Constructors

DOI10.2168/LMCS-7(1:2)2011zbMATH Open1218.03019arXiv1009.3429OpenAlexW4205386752MaRDI QIDQ3003303FDOQ3003303

Barbara Petit

Publication date: 26 May 2011

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1009.3429

zbMATH Keywords

pattern matchinglambda-calculuspolymorphismstrong normalisationreducibility candidates

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cited In (11)

• Type soundness for path polymorphism
• A Lambda-Calculus with Constructors
• Title not available (Why is that?)
• Typed path polymorphism
• One method of defining the semantics of programming language constructs in terms of lambda calculus. II
• Functional pearl: the distributive \(\lambda\)-calculus
• Continuation Models for the Lambda Calculus With Constructors
• A Polymorphic Type System for the Lambda-Calculus with Constructors
• The λ-calculus with constructors: Syntax, confluence and separation
• Title not available (Why is that?)
• On constructor rewrite systems and the lambda calculus

Uses Software

• OCaml

This page was built for publication: Semantics of Typed Lambda-Calculus with Constructors

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3003303)