Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence

DOI10.1007/978-3-540-87531-4_34MaRDI QIDQ3540198zbMATH OpenOpenAlexFDO

Authors Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano

Publication date 20 November 2008

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-87531-4_34

zbMATH Keywords

undecidabilityexistential typedomain-free type systemCPS-translation

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Type checking and typability in domain-free lambda calculi
• Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types
• Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems
• Typability and type checking in System F are equivalent and undecidable
• scientific article; zbMATH DE number 445160

Cites work

• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 1342279 (Why is no real title available?)
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Domain-free pure type systems
• Relational Parametricity and Control
• Representing Control: a Study of the CPS Transformation
• Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
• Typed Lambda Calculi and Applications
• Typing in pure type systems

Cited in

(13)

• scientific article; zbMATH DE number 445160 (Why is no real title available?)
• Existential type systems between Church and Curry style (type-free style)
• THE UNDECIDABILITY OF TYPE RELATED PROBLEMS IN TYPE -FREE STYLE SYSTEM F
• The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types
• CPS-translation as adjoint
• Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the π-Calculus
• Checking Emptiness of Non-Deterministic Regular Types with Set Operators
• Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems
• scientific article; zbMATH DE number 29189 (Why is no real title available?)
• Inhabitation of polymorphic and existential types
• Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types
• Existential Type Systems with No Types in Terms
• Type checking and typability in domain-free lambda calculi

This page was built for publication: Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence

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