EPJ Web of Conferences (Mar 2014)

Distributed Online Judge System for Interactive Theorem Provers

  • Mizuno Takahisa,
  • Nishizaki Shin-ya

DOI
https://doi.org/10.1051/epjconf/20146800016
Journal volume & issue
Vol. 68
p. 00016

Abstract

Read online

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.