Semantics of typed lambda-calculus with constructors

DOI10.2168/LMCS-7(1:2)2011MaRDI QIDQ3003303zbMATHOpenAlexFDO

Authors Barbara Petit

Publication date 26 May 2011

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

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)

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.

Recommendations

• A Polymorphic Type System for the Lambda-Calculus with Constructors
• A Lambda-Calculus with Constructors
• The λ-calculus with constructors: Syntax, confluence and separation
• scientific article; zbMATH DE number 4047683
• Inductive types and type constraints in the second-order lambda calculus

Cited in

(12)

• Continuation models for the lambda calculus with constructors
• scientific article; zbMATH DE number 1512607 (Why is no real title available?)
• Functional pearl: the distributive \(\lambda\)-calculus
• Inductive types and type constraints in the second-order lambda calculus
• A Polymorphic Type System for the Lambda-Calculus with Constructors
• The λ-calculus with constructors: Syntax, confluence and separation
• Typed path polymorphism
• On constructor rewrite systems and the lambda calculus
• A Lambda-Calculus with Constructors
• scientific article; zbMATH DE number 3854393 (Why is no real title available?)
• Type soundness for path polymorphism
• One method of defining the semantics of programming language constructs in terms of lambda calculus. II

Describes a project that uses

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)