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

DOI10.1007/978-3-642-11999-6_7MaRDI QIDQ3557097zbMATH OpenOpenAlexFDO

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

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)

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

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)