https://doi.org/10.1051/epjconf/20146800016
Distributed Online Judge System for Interactive Theorem Provers
1 Department of Computer Science, Tokyo Institute of Technology, Ookayama, Meguro, Tokyo 152-8552, Japan
Published online: 28 March 2014
In this paper, we propose a new software design of an online judge system for interactive theorem proving. The distinctive feature of this architecture is that our online judge system is distributed on the network and especially involves volunteer computing. In volunteers’ computers, network bots (software robots) are executed and donate computational resources to the central host of the online judge system. Our proposed design improves fault tolerance and security. We gave an implementation to two different styles of interactive theorem prover, Coq and ACL2, and evaluated our proposed architecture. From the experiment on the implementation, we concluded that our architecture is efficient enough to be used practically.
© Owned by the authors, published by EDP Sciences, 2014
This is an Open Access article distributed under the terms of the Creative Commons Attribution License 2.0, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
