El objetivo de este trabajo es verificar con Isabelle/HOL la segunda parte del curso de I1M. Más concretamente, los temas 14 a 22 dedicados a la representación funcional de estructuras de datos.
Dos trabajos con semejantes objetivos son:
- el curso Functional data structures (Summer semester 2017), impartido por Peter Lammich y Tobias Nipkow en la Universidad Técnica de Munich, en el que verifican con Isabelle/HOL algunas estructuras de datos.
- el trabajo de Andrew W. Appel Verified functional algorithms en el que verifica con Coq algunos algoritmos funcionales.
Los libros con aproximaciones funcionales a la algorítmica en la que se basan los trabajos anteriores son
- Purely functional data structures por C. Okasaki
- Algorithms: A functional programming approach por F. Rabhi y G. Lapalme
- Cálculo con números naturales.
- Propiedades de los números naturales.
- Ocurrencias de un elemento en una lista.
- Añadiendo los elementos al final de la lista e inversa.
- Plegados sobre árboles.
- Alineamientos de lista.
- Plegado de listas.
- Lista con elementos distintos.
- Plegados de listas por la derecha y por la izquierda.
- Cortes de listas.