Fusion theorem is a classical result that allows the simplification of the morphisms among homogeneus structures [10]. We present this theorem and some generalizations in the context of the constructive proof assistant tool Coq [2] where we have dependent types and parametric polymorphism. The work is organised as follows: afther the classical interpretation of the fusion law for catamorphisms in a categoric context, examples of fusion for programs defined with recursive types in Coq are analysed and the theorems of corresponding optimisation are shown. Finally, a generalisation of fusion law for inductive types is presented which is applied to a specific case. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Freire Nistal, J. L., Freire Branas, J. E., Ferro, A. B., & Sanchez Penas, J. J. (2001). Fusion in Coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2178 LNCS, pp. 583–596). Springer Verlag. https://doi.org/10.1007/3-540-45654-6_45
Mendeley helps you to discover research relevant for your work.