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

DOI10.1017/S0956796800001143zbMATH Open0827.03005OpenAlexW2112391755MaRDI QIDQ4764610FDOQ4764610

Authors: 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

Recommendations

• scientific article; zbMATH DE number 445157
• Typability and type checking in System F are equivalent and undecidable
• Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus

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

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

Cites Work

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

Cited In (18)

• Execution time of λ-terms via denotational semantics and intersection types
• Title not available (Why is that?)
• An analysis of the Core-ML language: Expressive power and type reconstruction
• Typability and type checking in System F are equivalent and undecidable
• Title not available (Why is that?)
• Complexity of type inference
• Title not available (Why is that?)
• Parameterized complexity: the main ideas and connections to practical computing
• Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
• Constrained minimum vertex cover in bipartite graphs: complexity and parameterized algorithms
• Non finitely generated types and λ-terms combinatoric representation cost
• Title not available (Why is that?)
• Parameterized computation and complexity: a new approach dealing with NP-hardness
• Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types
• Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus
• Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them
• The complexity ecology of parameters: An illustration using bounded max leaf number
• Title not available (Why is that?)

Uses Software

• Haskell
• Miranda

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

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