Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
Bruno Barras, Lourdes del Carmen Gonz\'alez Huesca, Hugo, Herbelin, Yann R\'egis-Gianas, Enrico Tassi, Makarius Wenzel and, Burkhart Wolff
TL;DR
This paper discusses the Paral-ITP project aimed at adapting proof assistants Isabelle and Coq for multicore systems to enhance their performance and scalability in interactive theorem proving.
Contribution
It introduces a comprehensive approach to enable parallelism in proof assistants, addressing the challenges of multicore integration.
Findings
Enhanced parallel processing capabilities in Isabelle and Coq
Improved scalability of interactive theorem proving
Framework for future multicore proof assistant development
Abstract
This is an overview of the Paral-ITP project, which intents to make the proof assistants Isabelle and Coq fit for the multicore era.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsCryptography and Data Security · Security and Verification in Computing · Logic, programming, and type systems