Principality and type inference for intersection types using expansion variables

DOI10.1016/j.tcs.2003.10.032zbMath1070.68021OpenAlexW2087381628MaRDI QIDQ1884929

J. B. Wells, A. J. Kfoury

Publication date: 27 October 2004

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2003.10.032

zbMATH Keywords

rank

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (19)

A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization ⋮ Principality and type inference for intersection types using expansion variables ⋮ Unnamed Item ⋮ Nominal essential intersection types ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Type Inference for Rank 2 Gradual Intersection Types ⋮ Non-Deterministic Functions as Non-Deterministic Processes (Extended Version) ⋮ Type inference for rank-2 intersection types using set unification ⋮ On strong normalization and type inference in the intersection type discipline ⋮ Strong normalization through intersection types and memory ⋮ De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Reasoning About Call-by-need by Means of Types ⋮ Inhabitation of Low-Rank Intersection Types ⋮ Implementing Compositional Analysis Using Intersection Types With Expansion Variables ⋮ Typability and type checking in System F are equivalent and undecidable ⋮ Essential and relational models ⋮ Elaborating intersection and union types

Uses Software

• ML
• GHC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Principal type schemes for an extended type theory
• Principal type scheme and unification for intersection type discipline
• An extension of basic functionality theory for \(\lambda\)-calculus
• Filter models with polymorphic types
• Typability and type checking in System F are equivalent and undecidable
• Bounded quantification is undecidable
• Principality and type inference for intersection types using expansion variables
• Functional Characters of Solvable Terms
• Type reconstruction in F_ω
• A modular, polyvariant and type-based closure analysis

This page was built for publication: Principality and type inference for intersection types using expansion variables