Skip to main content

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

Kriener, Jael and King, Andy and Blazy, Sandrine (2013) Proofs You Can Believe In: Proving Equivalences Between Prolog Semantics in Coq. In: Schrijvers, Tom, ed. Principles and Practice of Declarative Programming. ACM Press, New York, pp. 37-48. ISBN 978-1-4503-2154-9. (doi:10.1145/2505879.2505886) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:37524)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.
Official URL:
http://dx.doi.org/10.1145/2505879.2505886

Abstract

Basing program analyses on formal semantics has a long and successful tradition in the logic programming paradigm. These analyses rely on results about the relative correctness of mathematically sophisticated semantics, and authors 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. The results chosen are paradigmatic of the kind of correctness theorems that semantic analyses rely on and are therefore well-suited to explore the possibilities afforded by the application 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.

Item Type: Book section
DOI/Identification number: 10.1145/2505879.2505886
Subjects: A General Works
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 12 Dec 2013 13:26 UTC
Last Modified: 23 Apr 2022 22:07 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/37524 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.