1. Cezary Kaliszyk and Freek Wiedijk, Certified computer algebra on top of an interactive theorem prover, Towards Mechanized Mathematical Assistants, Lecture Notes in Computer Science, vol. 4573/2007, Springer Berlin / Heidelberg, 2007, pp. 94–105.