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

Jael Kriener 1 Andy King 1 Sandrine Blazy 2
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Type de document :
Communication dans un congrès
Tom Schrijvers. 15th International Symposium on Principles and Practice of Declarative Programming (PPDP), Sep 2013, Madrid, Spain. ACM, pp.37-48, 2013
Liste complète des métadonnées

Littérature citée [37 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00908848
Contributeur : Sandrine Blazy <>
Soumis le : lundi 25 novembre 2013 - 13:53:38
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : lundi 3 mars 2014 - 15:00:24

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00908848, version 1

Citation

Jael Kriener, Andy King, Sandrine Blazy. Proofs You Can Believe In. Proving Equivalences Between Prolog Semantics in Coq. Tom Schrijvers. 15th International Symposium on Principles and Practice of Declarative Programming (PPDP), Sep 2013, Madrid, Spain. ACM, pp.37-48, 2013. 〈hal-00908848〉

Partager

Métriques

Consultations de la notice

386

Téléchargements de fichiers

143