La Staff Week ‘Linear Algebra in Isabelle/HOL’, organizada en el marco del Seminario de Informática ‘Mirian Andrés’ 2017-2018, tiene lugar el 15, 16 y 17 de noviembre en la Universidad de La Rioja.
La creciente complejidad y la asignación de tareas críticas a los sistemas informáticos que se usan actualmente ha aumentado la preocupación sobre la corrección de los mismos; para estudiar esa corrección una de las herramientas más usadas son los «asistentes de demostración».
En estos entornos es posible modelar programas, especificar las propiedades que se espera que cumplan y, finalmente, demostrarlas (o detectar los posibles fallos). Muchas de las propiedades de los programas que se usan cada día se pueden expresar en términos matemáticos e, incluso, los propios programas pueden representar o resolver ciertos problemas matemáticos.
Una de las área de las Matemáticas más utilizadas es el Álgebra Lineal. A través del Álgebra Lineal podemos representar movimientos en el espacio (con aplicaciones a robótica o aeronáutica), calcular las variables más representativas de un problema o sistema complejo, analizar las propiedades de imágenes, modelizar fenómenos naturales…
En este seminario se analizarán las diferentes formulaciones que hay de Álgebra Lineal en el entorno Isabelle/HOL y cómo se pueda mejorar la comunicación entre ellas, de tal forma que se pueda reusar el trabajo hecho en una representación desde las otras.
La forma propuesta de trabajo es una reunión de un grupo reducido de especialistas de las Universidades de Cambridge, Munich, Innsbruck, Amsterdam y La Rioja que, por medio de diversas charlas y reuniones, tratarán de analizar y avanzar en los anteriores aspectos.
NOTA: Más información en https://seminariomirianandres.unirioja.es/sw17/.
