The complexity of type inference for higher-order typed lambda calculi

DOI10.1017/S0956796800001143zbMath0827.03005OpenAlexW2112391755MaRDI QIDQ4764610

Fritz Henglein, Harry G. Mairson

Publication date: 13 December 1995

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796800001143

zbMATH Keywords

lower boundscomplexity of type inferencedecidability of type inferenceencoding of Turing machines by typeshigher-order extensionssecond order polymorphic typed \(\lambda\)-calculus

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Theory of programming languages (68N15) Complexity of computation (including implicit computational complexity) (03D15) Combinatory logic and lambda calculus (03B40)

Related Items (6)

Constrained minimum vertex cover in bipartite graphs: complexity and parameterized algorithms ⋮ An analysis of the Core-ML language: Expressive power and type reconstruction ⋮ The complexity ecology of parameters: An illustration using bounded max leaf number ⋮ Parameterized Complexity ⋮ Typability and type checking in System F are equivalent and undecidable ⋮ Parameterized computation and complexity: a new approach dealing with NP-hardness

Uses Software

• Haskell
• Miranda

Cites Work

• Unnamed Item
• Unnamed Item
• A simple proof of a theorem of Statman
• Linear unification
• A theory of type polymorphism in programming
• The typed lambda-calculus is not elementary recursive
• On the sequential nature of unification
• Logic and programming languages
• Quantifier elimination and parametric polymorphism in programming languages
• On the Computational Complexity of Algorithms
• A Machine-Oriented Logic Based on the Resolution Principle
• The next 700 programming languages
• Intensional interpretations of functionals of finite type I
• The Principal Type-Scheme of an Object in Combinatory Logic

This page was built for publication: The complexity of type inference for higher-order typed lambda calculi