I1M2015: Comienzo del curso
El curso Informática (de 1º de Grado en Matemáticas) comenzarán el miércoles 23 de septiembre.
Las clases son los miércoles y viernes de 9:00 a 11:00.
La página con los materiales del curso se encuentra aquí.
Reseña: Case of (quite) painless dependently typed programming: Fully certified merge sort in Agda
Se ha publicado un artículo de razonamiento formalizado en Agda titulado Case of (quite) painless dependently typed programming: Fully certified merge sort in Agda.
Sus autores son Ernesto Copello, Álvaro Tasistro y Bruno Bianchi (del Grupo de Computación Teórica (Compute) en la Universidad ORT, Uruguay).
Su resumen es
We present a full certification of merge sort in the language Agda. It features: termination warrant without explicit proof, no proof cost to ensure that the output is sorted, and a succinct proof that the output is a permutation of the input.
El trabajo se ha presentado en The Brazilian Symposium on Programming Languages (SBLP).
El código de las correspondientes teorías en Agda se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.