Open Access
EPJ Web of Conferences
Volume 68, 2014
ICASCE 2013 – International Conference on Advances Science and Contemporary Engineering
Article Number 00016
Number of page(s) 5
Published online 28 March 2014
  1. L. C. Paulson, Logic and Computation: Interactive proof with Cambridge LCF, Cambridge University Press (1987) [CrossRef]
  2. Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions, Springer, 2004. [CrossRef]
  3. M. J. C. Gordon and T. F. Melham (editors), Introduction to HOL: A theorem proving environment for higher order logic, Cambridge University Press (1993)
  4. L. C. Paulson, Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, Vol. 828, Springer-Verlag (1994) [CrossRef]
  5. M. Kaufmann, P. Manolios, J. S. Moore, Computer-Aided Reasoning: An Approach, Kluwer Academic (2000)
  6. D. M. Russinoff, A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode, Formal Methods in System Design, Vol. 14, Issue 1, pp 75—125, Kluwer Academic (1999) [CrossRef]
  7. PC2 home page, (2013)
  8. Google Code Jam Home Page, (2013)
  9. S. Nishizaki, Programs with Continuations and Linear Logic, Science of Computer Programming, Vol. 21, No. 2, pp. 165—190, Elsevier (1994) [CrossRef]
  10. S. Nishizaki, A Polymorphic Environment Calculus and Its Type-Inference Algorithm, Higher-Order and Symbolic Computation, Vol. 13, No. 3, pp 239—278, Kluwer (2000). [CrossRef]
  11. T. Sasajima and S. Nishizaki, Blog-based Distributed Computation, Proceedings of ICICA2012, Lecture Notes in Computer Science, Vol. 7273, pp. 461–467, Springer (2012) [CrossRef]
  12. T. Mizuno and S. Nishizaki, Analyzing Systems Dependent on Execution Speed with Model Checker, Proceedings of ICASCE 2012, Procedia Engineering, Vol. 50, pp. 544—554, Elsevier (2012)