Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
DOI10.1007/978-3-540-87531-4_34zbMATH Open1156.03316OpenAlexW1592799753MaRDI QIDQ3540198FDOQ3540198
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
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
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)
Cites Work
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- Domain-free pure type systems
- Relational Parametricity and Control
- Typed Lambda Calculi and Applications
- Representing Control: a Study of the CPS Transformation
- Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
- Title not available (Why is that?)
- Typing in pure type systems
Cited In (13)
- 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
- Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the π-Calculus
- CPS-translation as adjoint
- 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
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
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)
