Descriptive and Relative Completeness ofLogics for Higher-Order Functions

Abstract. This paper establishes a strong completeness property of composi-tional program logics for pure and imperative higher-order functions introduced in [2, 15-18]. This property, called descriptive completeness, says that for eachprogram there is an assertion fully describing the former's behaviour up to the standard observational semantics. This formula is inductively calculable from theprogram text alone. As a consequence we obtain the first relative completeness result for compositional logics of pure and imperative call-by-value higher-orderfunctions in the full type hierarchy