Share  Bookmark

 Download from




 Funded by

1. M. Armand, B. Gregoire, A. Spiwack, and L. Thery. Extending Coq with imperative features and its application to SAT veri cation. In Interactive Theorem Proving, ITP 2010, Edinburgh, Scotland, July 1114, 2010, Proceedings, Lecture Notes in Computer Science. Springer, 2010.
2. A. Asperti, W. Ricciotti, C.S. Coen, and E. Tassi. Hints in uni cation. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, page 98. Springer, 2009.
3. A. Asperti, C. Sacerdoti Coen, E. Tassi, and S. Zacchiroli. User interaction with the Matita proof assistant. Journal of Automated Reasoning, 39(2):109{139, 2007.
4. G. Barthe, V. Capretta, and O. Pons. Setoids in type theory. J. Funct. Programming, 13(2):261{293, 2003. Special issue on \Logical frameworks and metalanguages".
5. Y. Bertot and P. Casteran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer Verlag, 2004.
6. Errett A. Bishop. Foundations of constructive analysis. McGrawHill Publishing Company, Ltd., 1967.
7. S. Boldo, J.C. Filli^atre, and G. Melquiond. Combining Coq and Gappa for Certifying FloatingPoint Programs. In Proceedings of the 16th Symposium, 8th International Conference. Held as Part of CICM'09 on Intelligent Computer Mathematics, page 74. Springer, 2009.
8. T. H. Brus, C. J. D. van Eekelen, M. O. van Leer, and M. J. Plasmeijer. Clean: A language for functional graph rewriting. In Proc. of a conference on Functional programming languages and computer architecture, pages 364{384, London, UK, 1987. SpringerVerlag.
9. V. Capretta. Universal algebra in type theory. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, TPHOLs 1999, volume 1690 of LNCS, pages 131{148. Springer, 1999.
10. J. Cartmell. Generalized algebraic theories and contextual categories. PhD thesis, University of Oxford, 1978.