A Prototype Proof Translator from HOL to Coq

1. [AHJ⁺OO]_A. Franke A, S.M. Hess, G.Ch. Jung, M. Kohlhase, and V. Sorge. Agent-oriented integration of distributed mathematical services. Journal of Universal Computer Science, 5, 2000.

   Google Scholar 

2. Henk Barendregt. The quest for correctness. Images of SMC research, pages 39–58, 1996. At ftp://ftp.cs.kun.nl/pub/CompMath.Found/quest.ps.Z.

3. [BBC⁺97]_Bruno Barras, Samuel Boutin, Cristina Cornes, Jean-Christophe Filliatre, Eduardo Giménez, Hugo Herbelin, Gerard Huet, Cesar Muñoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, and Benjamin Werner. The Coq Proof Assistant Reference Manual: Version 6.1. Technical Report RT-0203, Inria, May 1997.

   Google Scholar 

4. Robert S. Boyer and Gilles Dowek. Towards checking proof-checkers. In Workshop on Types for Proofs and Programs (Type’ 93), 1993.

   Google Scholar 

5. R. Boulton, K. Slind, A. Bundy, and M. Gordon. An interface between CLAM and HOL. In J. Grundy and M. Newey, editors, Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’98), volume 1479 of Lecture Notes in Computer Science, pages 87–104, Canberra, Australia, September/October 1998. Springer-Verlag.

   Chapter  Google Scholar 

6. O. Caprotti, D.P. Carlisle, and A.M. Cohen. Draft of the Open Math standard. The Open Math Society, 1999. http://www.nag.co.uk/projects/openmath/omsoc/.

7. A. P. Felty and D. J. Howe. Hybrid interactive theorem proving using Nuprl and HOL. In William McCune, editor, Proceedings of the 14th International Conference on Automated deduction, volume 1249 of LNAI, pages 351–365, Berlin, July 13–17 1997. Springer-Verlag.

   Google Scholar 

8. M. J. C. Gordon and Thomas F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.

   Google Scholar 

9. Fausto Giunchiglia, Paolo Pecchiari, and Carolyn Talcott. Reasoning theories: Towards an architecture for open mechanized reasoning systems. Technical Note CS-TN-94-15, Stanford University, Department of Computer Science, December 1994.

   Google Scholar 

10. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In Symposium on Logic in Computer Science, Ithaca, NY, pages 194–204. IEEE, June 1987.

    Google Scholar 

11. Necula and Lee. Efficient representation and validation of proofs. In LICS: IEEE Symposium on Logic in Computer Science, pages 93–104, 1998.

    Google Scholar 

12. Wai Wong. Validation of HOL proofs by proof checking. Formal Methods in System Design: An International Journal, 14(2):193–212, March 1999.

    Article  Google Scholar 

13. Vincent Zammit. A comparative study of Coq and HOL. In Elsa L. Gunter and Amy Felty, editors, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs’97, Murray Hill, NJ, USA, volume 1275 of Lecture Notes in Computer Science, pages 323–337. Springer-Verlag, August 1997.

    Google Scholar 

Download references