ML typability is DEXPTIME-complete

DOI10.1007/3-540-52590-4_50MaRDI QIDQ4027630zbMATH OpenFDO

Authors Assaf Kfoury, Jerzy Tiuryn, Paweł Urzyczyn

Publication date 21 February 1993

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-52590-4_50

zbMATH Keywords

acyclic semi-unificationanalysis of typabilityprogramming language ML

Mathematics Subject Classification ID

Theory of programming languages (68N15) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• An analysis of ML typability
• Haskell overloading is DEXPTIME-complete
• Typability and type checking in System F are equivalent and undecidable
• An algebraic characterization of typability in ML with subtyping
• scientific article; zbMATH DE number 88941

Cited in

(9)

• Extending the type checker of Standard ML by polymorphic recursion
• Haskell overloading is DEXPTIME-complete
• Almost every simply typed -term has a long -reduction sequence
• An algebraic characterization of typability in ML with subtyping
• An analysis of ML typability
• scientific article; zbMATH DE number 7029315 (Why is no real title available?)
• An analysis of the Core-ML language: expressive power and type reconstruction
• Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)
• The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types

This page was built for publication: ML typability is DEXPTIME-complete

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