Skip to Main content Skip to Navigation
Journal articles

Proof Checking and Logic Programming

Dale Miller 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [34 references]  Display  Hide  Download

https://hal.inria.fr/hal-01390901
Contributor : Dale Miller <>
Submitted on : Wednesday, November 2, 2016 - 3:38:30 PM
Last modification on : Thursday, March 5, 2020 - 6:33:42 PM
Long-term archiving on: : Friday, February 3, 2017 - 1:54:25 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

572

Files downloads

496