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

DOI10.1007/978-3-540-87531-4_34zbMath1156.03316OpenAlexW1592799753MaRDI QIDQ3540198

Makoto Tatsuta, Hiroshi Nakano, Koji Nakazawa, Yukiyoshi Kameyama

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

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

Related Items

Existential type systems between Church and Curry style (type-free style), Inhabitation of polymorphic and existential types, The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types, Existential Type Systems with No Types in Terms, CPS-translation as adjoint

Cites Work

• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Typing in pure type systems
• Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
• Representing Control: a Study of the CPS Transformation
• Domain-free pure type systems
• Relational Parametricity and Control
• Typed Lambda Calculi and Applications
• Unnamed Item
• Unnamed Item
• Unnamed Item