Pervasive parallelism in highly-trustable interactive theorem proving systems

DOI10.1007/978-3-642-39320-4_29MaRDI QIDQ2843039zbMATH OpenOpenAlexFDO

Authors Bruno Barras, Lourdes del Carmen González Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff

Publication date 9 August 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1305.7360

Mathematics Subject Classification ID

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.

Recommendations

• A parallelized theorem prover for a logic with parallel execution
• Shared-memory multiprocessing for interactive theorem proving
• scientific article; zbMATH DE number 1746646
• Interactive theorem proving from the perspective of Isabelle/Isar
• Overview on mechanized theorem proving

Cited in

(7)

• Parallelization of a hyper-linking-based theorem prover
• Bellerophon: tactical theorem proving for hybrid systems
• scientific article; zbMATH DE number 1086866 (Why is no real title available?)
• scientific article; zbMATH DE number 1746646 (Why is no real title available?)
• Shared-memory multiprocessing for interactive theorem proving
• A parallelized theorem prover for a logic with parallel execution
• A survey of interactive theorem proving

Describes a project that uses

Uses Software

• PIDE
• Isabelle/jEdit
• Coq
• Isabelle/Isar
• PolyML

This page was built for publication: Pervasive parallelism in highly-trustable interactive theorem proving systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2843039)