En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de datos de los conjuntos y tres de sus implementaciones en Haskell:
Las transparencias usadas en la clase son las del tema 117.
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado Echelon form.
Sus autores son Jose Divasón y Jesús Aransay (de la Universidad de la Rioja).
Su resumen es
We formalize an algorithm to compute the Echelon Form of a matrix. We have proved its existence over Bézout domains and made it executable over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This allows us to compute determinants, inverses and characteristic polynomials of matrices. The work is based on the HOL-Multivariate Analysis library, and on both the Gauss-Jordan and Cayley-Hamilton AFP entries. As a by-product, some algebraic structures have been implemented (principal ideal domains, Bézout domains, …). The algorithm has been refined to immutable arrays and code can be generated to functional languages as well.
El trabajo se ha publicado la semana pasada en The Archive of Formal Proofs
El código de las correspondientes teorías en Isabelle se encuentra aquí.
Se ha publicado un artículo sobre verifiación formal con Isabelle/HOL titulado Isabelle and security
Sus autores son
Su resumen es
Isabelle/HOL is a general-purpose proof assistant based on higher-order logic. Its main strengths are its simple-yet-expressive logic and its proof automation. Security researchers make up a significant fraction of Isabelle’s users. In the past few years, many exciting developments have taken place, connecting programming languages, operating system kernels, and security.
En la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios con el TAD de los polinomios presentados en la clase del día 11.
Los ejercicios y sus soluciones son
Read More “1M2104: Ejercicios con el TAD de los polinomios en Haskell”
Se ha publicado un artículo de razonamiento formalizado en Coq sobre titulado Machine-checked proofs for realizability checking algorithms.
Sus autores son
Su resumen es
We have recently proposed a contract-based realizability checking algorithm involving the use of theories, to provide an auxiliary procedure to consistency checking of “leaf-level” components in complex embedded systems. To prove the soundness of our approach on realizability, we formalized the necessary definitions and theorems of Towards realizability checking of contracts using theories, in the Coq proof and specification language.
El código de las correspondientes teorías en Coq se encuentra [aquí](.https://github.com/andrewkatis/Coq/
blob/master/realizability/Realizability.v).