Y. Bertot, P. Castéran, G. Huet, and C. Paulin-mohring, Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

W. Belkhir, A. Giorgetti, and M. Lenczner, A symbolic transformation language and its application to a multiscale method, Journal of Symbolic Computation, vol.65, pp.49-78, 2014.
DOI : 10.1016/j.jsc.2014.01.004
URL : https://hal.archives-ouvertes.fr/hal-00917323

B. J. Einar and L. Christoph, Theorem reuse by proof term transformation, Theorem Proving in Higher Order Logics, pp.152-167, 2004.

F. Baader and T. Nipkow, Term rewriting and all that, 1999.

R. [. Lenczner, W. Smith-yang, M. Belkhir, and . Lenczner, A two-scale model for an array of AFM's cantilever in the static case Computer-aided derivation of multiscale models: A rewriting framework, Mathematical and Computer Modelling International Journal for Multiscale Computational Engineering, vol.46, issue.122, pp.5-6776, 2007.

[. Yang, W. Belkhir, and M. Lenczner, COMPUTER-AIDED DERIVATION OF MULTISCALE MODELS: A REWRITING FRAMEWORK, International Journal for Multiscale Computational Engineering, vol.12, issue.2, pp.91-114, 2014.
DOI : 10.1615/IntJMultCompEng.2014006595
URL : https://hal.archives-ouvertes.fr/hal-00916568