Decidability of behavioural equivalence in unary PCF

DOI10.1016/S0304-3975(98)00024-3zbMath0914.68125MaRDI QIDQ1285665

Manfred Schmidt-Schauss

Publication date: 28 April 1999

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

zbMATH Keywords

PCFbehavioral equivalencesimply typed lambda calculusstrictness analysis

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Related Items (2)

Unnamed Item ⋮ Unary PCF is decidable

Uses Software

• Gofer

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Strictness analysis for higher-order functions
• A unification algorithm for typed \(\overline\lambda\)-calculus
• LCF considered as a programming language
• Fully abstract models of typed \(\lambda\)-calculi
• Unary PCF is decidable
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• Higher-order unification revisited: Complete sets of transformations
• Proving termination with multiset orderings
• The variable containment problem
• Full Abstraction and the Context Lemma
• Finitary PCF is not decidable

This page was built for publication: Decidability of behavioural equivalence in unary PCF