Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types

DOI10.1007/978-3-642-11999-6_7zbMATH Open1274.03027OpenAlexW1488396215MaRDI QIDQ3557097FDOQ3557097

Authors: Yuki Kato, Koji Nakazawa 

Publication date: 27 April 2010

Published in: Functional and Constraint Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-11999-6_7

Recommendations

• Type checking and typability in domain-free lambda calculi
• Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
• Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems
• The complexity of type inference for higher-order typed lambda calculi
• Inhabitation of types in the simply typed lambda calculus
• scientific article; zbMATH DE number 445155
• An extensible equality checking algorithm for dependent type theories
• Realizing the dependently typed \(\lambda\)-calculus
• Automated Deduction – CADE-20
• scientific article; zbMATH DE number 2185726

zbMATH Keywords

undecidabilitytype checkingtype inferenceexistential typedomain-free type system

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Cited In (3)

• Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems
• Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
• Type checking and typability in domain-free lambda calculi

This page was built for publication: Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types

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