Abstract
Nested datatypes can be defined in a Hindley-Milner system but it is difficult to implement functions on them. This paper analyzes the requirements that must be satisfied in order to implement programs (catamorphisms and anamorphisms) on these types. A solution, using Hagino's approach, is carried out here both in Haskell, using rank 2 signatures, and in the Coq proof assistant system where we have polymorphic recursion and also the capability to prove the correspondent programs specifications. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Blanco, A., Freire, J. E., & Freire, J. L. (2007). Using Coq to understand nested datatypes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4739 LNCS, pp. 210–216). Springer Verlag. https://doi.org/10.1007/978-3-540-75867-9_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
