Programación funcional y métodos elementales de demostración en Coq

PorJosé A. Alonso

En este tema se introduce mediante ejemplos la programación funcional en Coq y la demostración de las propiedades de las funciones definidas usando los métodos elementales de programación en Coq.

Su contenido es

  1. Datos y funciones
    1. Tipos enumerados
    2. Booleanos
    3. Tipos de las funciones
    4. Tipos compuestos
    5. Módulos
    6. Números naturales
  2. Métodos elementales de demostración
    1. Demostraciones por simplificación
    2. Demostraciones por reescritura
    3. Demostraciones por análisis de casos

La teoría correspondiente es

Resumen de lecturas compartidas durante junio de 2018

PorJosé A. Alonso
Esta entrada es una recopilación de lecturas compartidas, durante junio de 2018, en Twitter sobre programación funcional y demostración asistida por ordenador fundamentalmente.

Las lecturas están ordenadas según su fecha de publicación en Twitter.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Read More “Resumen de lecturas compartidas durante junio de 2018”