Type soundness for path polymorphism

DOI10.1016/j.entcs.2016.06.015zbMath1390.68170arXiv1601.03271OpenAlexW2233101269WikidataQ113317676 ScholiaQ113317676MaRDI QIDQ1744425

Eduardo Bonelli, Mauricio Ayala-Rincón, Andrés Viso

Publication date: 23 April 2018

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

zbMATH Keywords

pattern matching\(\lambda\)-calculusstatic typingpath polymorphism

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Data structures (68P05)

Related Items

Typed path polymorphism, Pure pattern calculus à la de Bruijn, Type soundness for path polymorphism, Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Type soundness for path polymorphism
• Subtyping recursion and parametric polymorphism in kernel Fun
• Efficient and flexible matching of recursive types
• The rewriting calculus - part II
• Pure patterns type systems
• Semantics of Typed Lambda-Calculus with Constructors
• First-class patterns
• Pattern Calculus
• The λ-calculus with constructors: Syntax, confluence and separation
• Efficient recursive subtyping
• An extension of system F with subtyping
• Computer Science Logic
• Typed Lambda Calculi and Applications
• Types for Proofs and Programs
• Programming Languages and Systems