Ponente: Jónathan Heras (Universidad de La Rioja)
Lugar: Seminario Chicho (Aula 314, Edificio Vives)
Hora: martes 30 de septiembre, 12:00
Coq
Hay 15 posts etiquetados con Coq.
Verifying a platform for digital imaging: a multi-tool strategy
Verifying an algorithm computing Discrete Vector Fields for digital imaging
Incidence simplicial matrices formalized in Coq/SSReflect
Hacia el procesamiento certificado de imágenes digitales. Parte II
Matrices de incidencia de complejos simpliciales en SSreflect: «after» Niza
Ponentes: María Poza (Universidad de La Rioja), Jónathan Heras (Universidad de La Rioja)
Lugar: Seminario Chicho (Aula 314, Edificio Vives)
Hora: jueves 7 de octubre, 13:00
En la charla nos informarán sobre los avances realizados en su exitosa estancia en el centro del INRIA de Sophia-Antipolis (Niza, Francia).
Matrices de incidencia de complejos simpliciales en SSreflect
Computing in Coq with Infinite Algebraic Data Structures
Small Scale reflection: an introduction (4 / 4)
Ponente: Yves Bertot (Inria, Sophia Antipolis), Laurence Rideau (Inria, Sophia Antipolis)
Lugar: Seminario Chicho (Aula 314, Edificio Vives)
Hora: jueves 24 de junio, 10:00 a 11:00, 16:30 a 17:30
Abstract: We propose a course in four parts around the «ssreflect» extension of the Coq system. The first part concerns the general structure of goals, scripts, and the main tactics. The second part concerns the main libraries to describe numbers, type structures, finite types, and so on. The third part concerns big operators and relies on an illustration on linear algebra. The fourth part concerns the general algebraic structures and their instantiation on known mathematical objects, with an illustration on the complex field.
Small Scale reflection: an introduction (3 / 4)
Ponente: Yves Bertot (Inria, Sophia Antipolis), Laurence Rideau (Inria, Sophia Antipolis)
Lugar: Seminario Chicho (Aula 314, Edificio Vives)
Hora: miércoles 23 de junio, 10:00 a 11:00, 16:30 a 17:30
Abstract: We propose a course in four parts around the «ssreflect» extension of the Coq system. The first part concerns the general structure of goals, scripts, and the main tactics. The second part concerns the main libraries to describe numbers, type structures, finite types, and so on. The third part concerns big operators and relies on an illustration on linear algebra. The fourth part concerns the general algebraic structures and their instantiation on known mathematical objects, with an illustration on the complex field.