The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types

DOI10.1016/j.ic.2012.07.003zbMath1283.03063OpenAlexW2081779849MaRDI QIDQ690505

Aleksy Schubert, Ken-etsu Fujita

Publication date: 27 November 2012

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2012.07.003

zbMATH Keywords

undecidabilitylambda calculussecond-order unificationtype checkingChurch-style type systemSystem FCurry-style type systemfinitely stratified polymorphic typespartial type inference

Mathematics Subject Classification ID

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

Related Items (1)

Existential type systems between Church and Curry style (type-free style)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Existential type systems between Church and Curry style (type-free style)
• CPS translations and applications: The cube and beyond
• Finitely stratified polymorphism
• The undecidability of the semi-unification problem
• Typability and type checking in System F are equivalent and undecidable
• A type inference algorithm for a stratified polymorphic type discipline
• On the undecidability of second-order unification
• The undecidability of the second order predicate unification problem
• Domain-Freeλµ-Calculus
• Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
• Existential Type Systems with No Types in Terms
• THE UNDECIDABILITY OF TYPE RELATED PROBLEMS IN TYPE -FREE STYLE SYSTEM F

This page was built for publication: The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types