Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting
| Autor: | Michael Färber |
|---|---|
| Přispěvatelé: | University of Innsbruck, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Leopold Franzens Universität Innsbruck - University of Innsbruck |
| Rok vydání: | 2022 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science reduction 0102 computer and information sciences 02 engineering and technology 01 natural sciences Dedukti type checking 0202 electrical engineering electronic engineering information engineering concurrency Interactive proof systems CCS Concepts: • Theory of computation → Logic and verification Equational logic and rewriting [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering Automated reasoning Higher order logic concurrency Logic in Computer Science (cs.LO) rewriting sharing TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Rust 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS verification performance |
| Zdroj: | 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’22) 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’22), Jan 2022, Philadelphia, PA, United States. ⟨10.1145/3497775.3503683⟩ |
| DOI: | 10.1145/3497775.3503683 |
| Popis: | Several proof assistants, such as Isabelle or Coq, can concurrently check multiple proofs. In contrast, the vast majority of today's small proof checkers either does not support concurrency at all or only limited forms thereof, restricting the efficiency of proof checking on multi-core processors. This work shows the design of a small, memory- and thread-safe kernel that efficiently checks proofs both concurrently and non-concurrently. This design is implemented in a new proof checker called Kontroli for the lambda-Pi calculus modulo rewriting, which is an established framework to uniformly express a multitude of logical systems. Kontroli is faster than the reference proof checker for this calculus, Dedukti, on all of five evaluated datasets obtained from proof assistants and interactive theorem provers. Furthermore, Kontroli reduces the time of the most time-consuming part of proof checking using eight threads by up to 6.6x. 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '22), Jan 2022, Philadelphia, PA, United States |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|