R. Bird, Constructive functional programming, In: STOP Summer School on Constructive Algorithmics, Abeland, 1989.
DOI : 10.1007/978-3-642-74884-4_5

A. Kaldewaij, Programming: the derivation of algorithms, 1990.

R. Bird and O. De-moor, The Algebra of Programming, 1996.
DOI : 10.1007/978-3-642-61455-2_12

R. Bird, An Introduction to the Theory of Lists, Logic of Programming and Calculi of Discrete Design, pp.5-42, 1987.
DOI : 10.1007/978-3-642-87374-4_1

J. Gibbons, Algebras for Tree Algorithms Available as Technical Monograph PRG-94, 1991.

O. De-moor, Categories, relations and dynamic programming, 1992.

Z. Hu, M. Takeichi, and W. N. Chin, Parallelization in calculational forms, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.316-328, 1998.
DOI : 10.1145/268946.268972

D. R. Smith, KIDS ? a knowledge-based software development system, pp.483-514, 1991.

O. De-moor and G. Sittampalam, Generic Program Transformation, Third International Summer School on Advanced Functional Programming, 1998.
DOI : 10.1007/10704973_3

T. Yokoyama, Z. Hu, and M. Takeichi, Yicho: A system for programming program calculations, 2002.

Y. Bertot and P. Casteran, Interactive Theorem Proving and Program Development ? Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

M. Sozeau and N. Oury, First-Class Type Classes, p.8, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864

E. Visser, A survey of strategies in rule-based program transformation systems, Journal of Symbolic Computation, vol.40, issue.1, pp.831-873, 2005.
DOI : 10.1016/j.jsc.2004.12.011

S. C. Mu, H. S. Ko, and P. Jansson, Algebra of programming in Agda: Dependent types for relational program derivation, Journal of Functional Programming, vol.5, issue.05, pp.545-579, 2009.
DOI : 10.1016/j.scico.2003.09.003

L. Augustsson, Cayenne -a language with dependent types, International Conference on Functional Programming, pp.239-250, 1998.

C. Mcbride, Epigram: Practical Programming with Dependent Types, Lecture Notes in Computer Science, vol.3622, pp.130-170, 2004.
DOI : 10.1007/11546382_3

U. Norell, Dependently typed programming in agda, pp.1-2, 2009.

P. Corbineau, A Declarative Language for the Coq Proof Assistant, TYPES '07, pp.69-84, 2007.
DOI : 10.1007/978-3-540-68103-8_5