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 calculusDecidabilityFull abstractionPCF

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Related Items (19)

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

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

This page was built for publication: Finitary PCF is not decidable