He actualizado el libro Exámenes de programación funcional con Haskell. El libro es una recopilación de los exámenes de la asignatura de Informática (de primero del Grado en Matemáticas) desde el curso 30 de noviembre de 2009 al 15 de septiembre de 2014.
Tras la ampliación, el libro contiene 129 exámenes y 833 ejercicios.
Este libro es el complemento de los anteriores:
Se ha publicado un artículo de razonamiento formalizado en Coq titulado Hofstadter’s problem for curious readers.
Su autor es Pierre Letouzey (del grupo PPS (Preuves, Programmes et Systèmes) de la Universidad de París VII Denis Diderot, Francia).
Su resumen es
This document summarizes the proofs made during a Coq development in Summer 2015. This development investigates the function G introduced by Hofstadter in his famous “Gödel, Escher, Bach” book as well as a related infinite tree. The left/right flipped variant of this G tree has also been studied here, following Hofstadter’s “problem for the curious reader”. The initial G function is refered as sequence A005206 in OEIS, while the flipped version is the sequence A123070.
The detailed and machine-checked proofs can be found in the files of
this development and can be re-checked by running Coq version 8.4 on it. No prior knowledge of Coq is assumed here, on the contrary this document has rather been a “Coq-to-English” translation exercise for the author. Nonetheless, some proofs given in this document are still quite sketchy: in this case, the interested reader is encouraged to consult the Coq files given as references.
El código de las correspondientes teorías en Coq 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.
Se ha publicado un artículo de automatización del razonamiento en Isabelle/HOL titulado Deriving comparators and show functions in Isabelle/HOL.
Sus autores son Christian Sternagel y René Thiemann (del Computational Logic Research Group en la Universidad de Innsbruck, Austria).
Su resumen es
We present an Isabelle/HOL development that allows for the automatic generation of certain operations for user-defined datatypes. Since the operations are defined within the logic, they are applicable for code generation. Triggered by the demand to provide readable error messages as well as to access efficient data structures like sorted trees in generated code, we provide show functions that compute the string representation of a given value, comparators that yield linear orders, and hash functions. Moreover, large parts of the employed machinery should be reusable for other operations like read functions, etc.
In contrast to similar mechanisms, like Haskell’s “deriving,” we do not only generate definitions, but also prove some desired properties, e.g., that a comparator indeed orders values linearly. This is achieved by a collection of tactics that discharge the corresponding proof obligations automatically.
El trabajo se presentó el 25 de agosto en el ITP 2015 (The 6th conference on Interactive Theorem Proving).
El código de las correspondientes teorías en Isabelle/HOL 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.
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í.
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.