I1M2013: Introducción a la programación con Haskell

PorJosé A. Alonso

En la segunda parte de la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se ha presentado una introducción a la programación con Haskell usando emacs como entorno de programación. Concretamente, se ha explicado cómo

  • usar Haskell como calculadora aritmética (con las funciones +, -, *, /, div y ^).
  • escribir guiones de Haskell en emacs.
  • cargar los guiones y evaluar expresiones con las funciones definidas.

Como tarea para la próxima clase se ha propuesto instalar GHC y emacs (cuyos enlaces se encuentran en la página de sistemas y escribir de manera colaborativa las soluciones de los ejercicios de la 1º relación y de la 2º relación.

Las sesiones se encuentran grabadas en dos vídeos:

  • en el primer vídeo se muestra cómo trabajar con guiones en Haskell dentro de emacs,
  • en el segundo vídeo se muestra cómo trabajar con las relaciones de ejercicios y la wiki.

Las transparencias usadas en la clase son las del tema 2:
Read More “I1M2013: Introducción a la programación con Haskell”

I1M2013: Presentación del curso de Informática (de 1º de Matemáticas)

PorJosé A. Alonso

En la primera parte de la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se ha presentado la asignatura siguiendo el resumen del proyecto docente y los materiales en la página de la asignatura:

Se ha explicado cómo instalar los sistemas y se ha mostrado una sesión sobre el uso de Haskell y emacs. La sesión está grabada en este vídeo.

Se ha comentado el sistema de evaluación y se ha anunciado las fechas de los exámenes de todo el curso.

Proof assistant based on didactic considerations

PorJosé A. Alonso

Se ha publicado un artículo sobre el uso de sistemas de razonamiento en la enseñanza de la lógica titulado Proof assistant based on didactic considerations.

Sus autores son Jorge Pais y Álvaro Tasistro (de la Universidad ORT Uruguay, Uruguay).

Su resumen es

We consider some issues concerning the role of Formal Logic in Software Engineering education, which lead us to promote the learning of formal proof through extensive, appropriately guided practice. To this end, we propose to adopt Natural Deduction as proof system and to make use of an adequate proof assistant to carry out formal proof on machine. We discuss some necessary characteristics of such proof assistant and subsequently present the design and implementation of our own version of it. This incorporates several novel features, such as the display and edition of derivations as trees, the use of meta-theorems (derived rules) as lemmas, and the possibility of maintaining a set of draft trees that can be inserted into the main derivation as needed. The assistant checks the validity of each edition operation as performed. So far, it has been implemented for propositional logic and (quite satisfactorily) put into practice in courses of Logic for Software Engineering and Information Systems programs.

El artículo se ha publicado en Journal of Universal Computer Science.