Reseña: Experience report: Teaching Haskell to the masses

PorJosé A. Alonso

Se ha publicado un artículo sobre la ensñanza de Haskell titulado Experience report: Teaching Haskell to the masses.

Sus autores son Jasmin Christian Blanchette, Tobias Nipkow, Lars Noschinski y Dmitriy Traytel (de la Universidad Técnica de Munich).

Su resumen es

We report on our experience teaching a Haskell-based functional programming course to over 600 students. The syllabus was organized around selected material from various sources. Throughout the term, we emphasized correctness through QuickCheck tests and proofs by induction. The submission architecture was coupled with automatic testing, giving students the possibility to correct mistakes before the deadline. To motivate the students, we complemented the weekly assignments with an informal competition.

Reseña: Square root and division elimination in PVS

PorJosé A. Alonso

Se ha publicado un artículo de automatización del razonamiento en PVS titulado Square root and division elimination in PVS.

Su autor es Pierre Neron (del INRIA en Paris – Rocquencourt).

El trabajo se presentará en julio en el ITP 2013 (4th Conference on Interactive Theorem Proving).

Su resumen es

In this paper we present a new strategy for PVS that implements a square root and division elimination in order to use automatic arithmetic strategies that were not able to deal with these operations in a first place. This strategy relies on a PVS formalization of the square root and division elimination and deep embedding of PVS expressions inside PVS. Therefore using computational reflection and symbolic computation we are able to automatically transform expressions into division and square root free ones before using these decisions procedures.

El código de las correspondientes teorías PVS se encuentra aquí.