En la clase de hoy del curso de Razonamiento automático se ha visto cómo se puede en Isabelle/HOL
El Grupo de automatización de la Lógica (del Instituto Max Planck en Saarbrücken, Alemania) ha publicado una oferta de plaza: PhD/Project Position.
La investigación se centrará en la integración de un sistema de razonamiento automático (SPASS) con otro interactivo (Isabelle).
El trabajo será dirigido por Christoph Weidenbach y se desarrollará en cooperación con el Grupo de demostración automática de la Universidad de Munich que dirige Tobias Nipkow.
El objetivo de la clase de hoy es aprender, resolviendo ejercicios, a definir funciones en Haskell usando las listas de comprensión introducidas en el tema 5.
En concreto, se han comentado la solución de los ejercicios 5, 6, 7 y 8 de la 5ª relación y los ejercicios 4.2, 4.3, 5.1 y 5.2 de la 6ª relación
Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los ejercicios de la 7ª relación y de la de la 8ª relación.
He publicado en la página de ejercicios del curso de Informática (de 1º del Grado en Matemáticas) los enlaces a tres libros de problemas resueltos de programación en Haskell que he escrito estos años.
Los libros son los siguientes:
El Grupo de métodos formales de la Universidad de Twente ha ofertado 2 plazas para trabajar en Enschede (Países Bajos): PhD and Post Doc position on ERC project Verifcation of Concurrent Data Structures (U. Twente, Netherlands)
El trabajo consistirá en la especificación y verificación de estructuras de datos concurrentes.
Las dos plazas se incriben en el proyecto VerCors (Verification of Concurrent Data Structures) dirigido por Marieke Huisman.