Asistentes de prueba y verificación formal

http://hablandodematematicas.matem.unam.mx

Resumen: 

El uso de las computadoras para automatizar tareas es una práctica común, inclusive es posible realizar demostraciones matemáticas usando herramientas computacionales diseñadas para ello.
En esta plática veremos un acercamiento a la verificación formal dentro del área de Métodos Formales en Ciencias de la Computación y comentaremos los principios de los sistemas interactivos para el manejo de demostraciones que facilitan la verificación de sistemas y formalizaciones matemáticas.

En particular, nos enfocaremos en el asistente llamado Coq que también es considerado como un ambiente de desarrollo para la programación certificada.