Finitary PCF is not decidable

DOI10.1016/S0304-3975(00)00194-8zbMath0992.68017WikidataQ29396610 ScholiaQ29396610MaRDI QIDQ5958762

No author found.

Publication date: 3 March 2002

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

Lambda calculus; Decidability; Full abstraction; PCF

Mathematics Subject Classification ID

68N15: Theory of programming languages

68N18: Functional programming and lambda calculus

Related Items

Unnamed Item, Unnamed Item, Computing with Functionals—Computability Theory or Computer Science?, An observationally complete program logic for imperative higher-order functions, Program equivalence in a simple language with state, The extensional ordering of the sequential functionals, Operational domain theory and topology of sequential programming languages, Natural non-dcpo domains and f-spaces, Unary PCF is decidable, Decidability of behavioural equivalence in unary PCF, Relative definability of boolean functions via hypergraphs, The sequentially realizable functionals, Full abstraction for PCF, An approach to deciding the observational equivalence of Algol-like languages, Decidability and syntactic control of interference, A relational account of call-by-value sequentiality, Exploratory Functions on Nondeterministic Strategies, up to Lower Bisimilarity, Definability and Full Abstraction, Typing Weak MSOL Properties

Cites Work

• LCF considered as a programming language
• Fully abstract models of typed \(\lambda\)-calculi
• Unary PCF is decidable
• Polymorphic rewriting conserves algebraic confluence
• On full abstraction for PCF: I, II and III
• Kripke logical relations and PCF
• Logical relations and the typed λ-calculus
• Decidability of all minimal models
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item