Proofs You Can Believe In Proving Equivalences Between Prolog Semantics in Coq

Basing program analyses on formal semantics has a long and successful tradi-tion in the logic programming paradigm. These analyses rely on results about the relative correctness of mathematically sophisticated semantics, and au-thors of such analyses often invest considerable effort into establishing these results. The development of interactive theorem provers such as Coq and their recent successes both in the field of program verification as well as in mathematics, poses the question whether these tools can be usefully deployed in logic programming. This paper presents formalisations in Coq of several general results about the correctness of semantics in different styles; forward and backward, top-down and bottom-up. It also presents a formalisation of stratification, which is a semantic construction that enables a logically consis-tent meaning to be assigned to Prolog programs, rather than idealised logic programs, which employ cut and negation. The results chosen are paradig-matic of the kind of correctness theorems that semantic analyses rely on and are therefore well-suited to explore the possibilities afforded by the appli-cation of interactive theorem provers to this task, as well as the difficulties likely to be encountered in the endeavour. It turns out that the advantages offered by moving to a functional setting, including the possibility to apply higher-order abstract syntax, are considerable