19.4.06
Paper: Descriptive and Relative Completeness of Logics for Higher-Order Functions
By Kohei Honda, Martin Berger, and Nobuko Yoshida.
[Phil's comment: The program logic itself looks remarkably straightforward.]
Abstract. This paper establishes a strong completeness property of compositional program logics for pure and imperative higher-order functions introduced in earlier work by the authors. This property, called descriptive completeness, says that for each program there is an assertion fully describing the former’s behaviour up to the standard observational semantics. This formula is inductively calculable from the program text alone. As a consequence we obtain the first relative completeness result for compositional logics of pure and imperative call-by-value higher-order functions in the full type hierarchy.
[Phil's comment: The program logic itself looks remarkably straightforward.]
Abstract. This paper establishes a strong completeness property of compositional program logics for pure and imperative higher-order functions introduced in earlier work by the authors. This property, called descriptive completeness, says that for each program there is an assertion fully describing the former’s behaviour up to the standard observational semantics. This formula is inductively calculable from the program text alone. As a consequence we obtain the first relative completeness result for compositional logics of pure and imperative call-by-value higher-order functions in the full type hierarchy.
