[TYPES/announce] Paper on Higher-Order Subtyping
Martin Berger
martinb at dcs.qmul.ac.uk
Thu Apr 6 08:08:17 EDT 2006
Hello colleagues, we'd like to announce a new paper.
Descriptive and Relative Completeness of Logics for Higher-Order
Functions
available at http://www.dcs.qmul.ac.uk/~martinb/publications/completeness
Abstract: This paper establishes a strong completeness property of
compositional program logics for pure and imperative higher-order
functions introduced 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.
Your comments and though are highly appreciated.
Best wishes,
Kohei Honda, Nobuko Yoshida, Martin Berger
More information about the Types-announce
mailing list