El Grupo de verificación formal de la Universidad de Oxford ha a anunciado una oferta de trabajo.
El trabajo se realizará dentro del proyecto PINCETTE y será dirigido por Daniel Kröning.
Los detalles del trabajo pueden consultarse aquí.
El Departamento de Ciencias de la Computación de la Universidad de Yale
ha pubicado una oferta de trabajo en temas de Lógica Computacional: PostDoc and PhD Positions at Yale University
El objetivo del trabajo es el desarrollo de un nuevo sistema operativo cuyo núcleo esté formalmente certificado. Una descripción detallada del mismo se encuentra en Advanced Development of Certified OS Kernels.
El trabajo se desarrollará en el grupo FLINT y será dirigido por Zhong Shao y Bryan Ford.
El objetivo de la clase de hoy es el mismo de la clase anterior: aprender, resolviendo ejercicios, a definir funciones en Haskell mediante los procedimientos básicos estudiados en el tema 4.
En concreto, se han resuelto los siguientes ejercicios:
Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los restantes ejercicios de la 4ª relación.
El objetivo de la clase de hoy es el mismo de la clase anterior: aprender, resolviendo ejercicios, a definir funciones en Haskell mediante los procedimientos básicos estudiados en el tema 4.
En concreto, se han resuelto los ejercicios 7 (mitades), 8 (tailSeguro), 9 (disj), 11 (maxI) y 12 (menorMultiplo) de la 2ª relación y el ejercicio 1 (raices) de la 3ª relación
Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los restantes ejercicios de la 3ª relación y los ejercicios de la 4ª relación.
El objetivo de la de hoy es aprender, resolviendo ejercicios, a definir funciones en Haskell mediante los procedimientos básicos y comprobar sus propiedades con QuickCheck.
En concreto, se han resuelto los ejercicios 4 (iniciales), 5 (prop_iniciales_ultimo), 6.1, 6.2 (cambioEuro), 6.3 (pesetas), 6.4 (euros), 6.5 (prop_EurosPesetas), 6.6, 6.7 y 11.1 (maxI) de la 2ª relación.
Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los restantes ejercicios de la 2ª relación y los ejercicios de la 3ª relación.