Computing Publications

Publications Home » Descriptive and Relative Complete...

Descriptive and Relative Completeness of Logics for Higher-Order Functions

Kohei Honda, Martin Berger, Nobuko Yoshida

Conference or Workshop Paper
ICALP'06, The 33rd International Colloquium on Automata, Languages and Programming
The 33rd International Colloquium on Automata, Languages and Programming
July, 2006
Springer Verlag
Abstract

This paper establishes a strong completeness property of compositional

program logics for pure and imperative higher-order functions

introduced in cite{HY04PPDP,SHORT1,SHORTLONG,GLOBAL,ALIAS}. This

property, called {em descriptive completeness}, says that for each

program there is an assertion fully describing the program'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.

BibTEX file for the publication
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.