Reseña: A short Isabelle/HOL tutorial for the functional programmer

Se ha publicado un tutorial de razonamiento formalizado con Isabelle/HOL titulado A short Isabelle/HOL tutorial for the functional programmer.

Su autor es Thomas Genet (de la Universidad de Rennes 1, Francia).

Su resumen es

The objective of this (very) short tutorial is to help any functional programmer to quickly put its hand on Isabelle/HOL and catch a glimpse of its power. Then, if you want some more, you should refer to the extensive Isabelle/HOL tutorial and documentation available in the tool.

Este tutorial puede servir de lectura complementaria en los cursos de Lógica matemática y fundamentos, Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.