Skip to Main content Skip to Navigation
New interface
Journal articles

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
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 metadata

Cited literature [34 references]  Display  Hide  Download
Contributor : Dale Miller Connect in order to contact the contributor
Submitted on : Wednesday, November 2, 2016 - 3:38:30 PM
Last modification on : Friday, July 8, 2022 - 10:04:57 AM
Long-term archiving on: : Friday, February 3, 2017 - 1:54:25 PM


Files produced by the author(s)



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



Record views


Files downloads