Unary PCF is Decidable

We show that unary PCF, a very small fragment of Plotkin’s PCF [?], cidable observational pre-order, and that its fully abstract model is effectively presentable. This is in marked contrast to larger fragments, where corresponding results fail [?]. The techniques used are adaptions of those of Padovani [?], who applied them to the minimal model of the simply typed lambda calculus.

• Type: Journal
• Year: 1998
• Where: TCS
• Authors: Ralph Loader
• Keywords: Cidable Observational Pre-order, Simply Typed Lambda Calculus, TCS 1998, Theoretical Computer Science, Unary Pcf