Shared-memory multiprocessing for interactive theorem proving

DOI10.1007/978-3-642-39634-2_30MaRDI QIDQ5327360zbMATH OpenOpenAlexFDO

Authors Makarius Wenzel

Publication date 7 August 2013

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39634-2_30

Mathematics Subject Classification ID

Recommendations

• Pervasive parallelism in highly-trustable interactive theorem proving systems
• A parallelized theorem prover for a logic with parallel execution
• Asynchronous user interaction and tool integration in Isabelle/PIDE
• Interactive theorem proving from the perspective of Isabelle/Isar
• The Isabelle Framework

Cited in

(7)

• From LCF to Isabelle/HOL
• Toward sharing libraries of mathematics between theorem provers
• Pervasive parallelism in highly-trustable interactive theorem proving systems
• Mechanizing a process algebra for network protocols
• Collaborative Interactive Theorem Proving with Clide
• A parallelized theorem prover for a logic with parallel execution
• Distributed parallel build for the Isabelle archive of formal proofs

Describes a project that uses

Uses Software

• Isabelle/jEdit
• Archive Formal Proofs

This page was built for publication: Shared-memory multiprocessing for interactive theorem proving

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