PCF

In the general sense, “PCF” means a simply-typed lambda calculus with a small number of base types, a few primitive constructs, and a fixed-point combinator.

Archetypally, the base types are just booleans and natural numbers, and the primitive constructs are constants (boolean and numeric literals), conditionals, an “is zero?” test, and successor and predecessor maps.

PCF was first described in Plotkin 1977 as programming language analogue to Dana Scott's combinatory system LCF.

Plotkin's original paper doesn't tell us what PCF stands for, but we can infer that “CF” stands for “computable functions” and that “P” stands for something with the stem “program”. Wikipedia's article is titled “Programming Computable Functions”, but the lede also gives “Programming with Computable Functions” and “Programming language for Computable Functions” as possible meanings.