Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting

Autor: Michael Färber

Publikováno v: 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⟩

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 effici

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5cddaf3514c7efb51783a8e3c025fc24
https://doi.org/10.1145/3497775.3503683