Proof Checking and Logic Programming

Dale Miller 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : In a world where trusting software systems is increasingly important, formal methods and formal proof can help provide trustable foundations. Proof checking can help to reduce the size of the trusted base since we do not need to trust an entire theorem prover if we can check the proofs they produce by a trusted (and smaller) checker. Many approaches to building proof checkers require embedding within them a full programming language. In most many modern proof checkers and theorem provers, that programming language is a functional programming language, often a variant of ML. In fact, parts of ML (e.g., strong typing , abstract datatypes, and higher-order programming) were designed to make ML into a trustworthy " metalanguage " for checking proofs. While there is considerable overlap in the foundations of logic programming and proof checking (both benefit from unification, backtracking search, efficient term structures, etc), the discipline of logic programming has, in fact, played a minor role in the history of proof checking. I will argue that logic programming can have a major role in the future of this important topic.
Type de document :
Article dans une revue
Formal Aspects of Computing, Springer Verlag, 2017, 29 (3), pp.383-399 〈10.1007/s00165-016-0393-z〉
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger
Contributeur : Dale Miller <>
Soumis le : mercredi 2 novembre 2016 - 15:38:30
Dernière modification le : mercredi 25 avril 2018 - 10:45:27
Document(s) archivé(s) le : vendredi 3 février 2017 - 13:54:25


Fichiers produits par l'(les) auteur(s)



Dale Miller. Proof Checking and Logic Programming. Formal Aspects of Computing, Springer Verlag, 2017, 29 (3), pp.383-399 〈10.1007/s00165-016-0393-z〉. 〈hal-01390901〉



Consultations de la notice


Téléchargements de fichiers