Reseña: Case of (quite) painless dependently typed programming: Fully certified merge sort in Agda

PorJosé A. Alonso

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.