Ackermann’s Function in Iterative Form: A Proof Assistant Experiment

Termination is an important property of programs, and is notably required for programs formulated in proof assistants. It is a very active subject of research in the Turing-complete formalism of term rewriting. Over the years, many methods and tools have been developed to address the problem of deciding termination for specific problems (since it is undecidable in general). Ensuring the reliability of those tools is therefore an important issue.In this paper we present a library formalising important results of the theory of well-founded (rewrite) relations in the proof assistant Coq. We also present its application to the automated verification of termination certificates, as produced by termination tools.The sources are freely available athttp://color.inria.fr/.

Download Full-text

Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

Mathematical Structures in Computer Science ◽

10.1017/s0960129521000335 ◽

2021 ◽

pp. 1-20

Author(s):

Ernesto Copello ◽

Nora Szasz ◽

Álvaro Tasistro

Keyword(s):

Type Theory ◽

Lambda Calculus ◽

Proof Assistant ◽

First Order ◽

Constructive Type Theory ◽

Fundamental Part ◽

Constructive Type ◽

Free Variables ◽

The Church ◽

Theoretical Results

Abstarct We formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. As a fundamental part of the formalization, we introduce principles of induction and recursion on terms which provide a framework for reproducing the use of the Barendregt Variable Convention as in pen-and-paper proofs within the rigorous formal setting of a proof assistant. The principles in question are all formally derivable from the simple principle of structural induction/recursion on concrete terms. We work out applications to some fundamental meta-theoretical results, such as the Church–Rosser Theorem and Weak Normalization for the Simply Typed Lambda Calculus. The whole development has been machine checked using the system Agda.

Download Full-text

Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant

Automated Deduction – CADE 28 - Lecture Notes in Computer Science ◽

10.1007/978-3-030-79876-5_26 ◽

2021 ◽

pp. 450-467

Author(s):

Hans-Jörg Schurr ◽

Mathias Fleury ◽

Martin Desharnais

Keyword(s):

Success Rate ◽

Failure Rate ◽

Proof Assistant ◽

Proof Checking ◽

Smt Solver ◽

Fine Grained ◽

Simple Rules ◽

Detailed Evaluation ◽

Reconstruction Time

AbstractWe present a fast and reliable reconstruction of proofs generated by the SMT solver veriT in Isabelle. The fine-grained proof format makes the reconstruction simple and efficient. For typical proof steps, such as arithmetic reasoning and skolemization, our reconstruction can avoid expensive search. By skipping proof steps that are irrelevant for Isabelle, the performance of proof checking is improved. Our method increases the success rate of Sledgehammer by halving the failure rate and reduces the checking time by 13%. We provide a detailed evaluation of the reconstruction time for each rule. The runtime is influenced by both simple rules that appear very often and common complex rules.

Download Full-text