Semantics of typed lambda-calculus with constructors
From MaRDI portal
Publication:3003303
DOI10.2168/LMCS-7(1:2)2011zbMATH Open1218.03019arXiv1009.3429OpenAlexW4205386752MaRDI QIDQ3003303FDOQ3003303
Authors: 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
Recommendations
Cited In (12)
- Inductive types and type constraints in the second-order lambda calculus
- 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
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)
