En la sesión de hoy del Seminario de Lógica Computacional Ángel Ruiz Campos ha explicado la programación funcional en Coq.
La teoría, junto con los ejercicios, utilizados en la exposición son
Read More “SLC2018: Programación funcional en Coq”
Se ha publicado un artículo de razonamiento formalizado en Coq sobre álgebra titulado Formalized linear algebra over elementary divisor rings in Coq.
Sus autores son
Su resumen es
This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main results are the formalization that these rings support essential operations of linear algebra, the classification theorem of finitely presented modules over such rings and the uniqueness of the Smith normal form up to multiplication by units. We present formally verified algorithms computing this normal form on a variety of coefficient structures including Euclidean domains and constructive principal ideal domains. We also study different ways to extend Bézout domains in order to be able to compute the Smith normal form of matrices. The extensions we consider are: adequacy (i.e. the existence of a gdco operation), Krull dimension ≤1 and well-founded strict divisibility.
El trabajo se ha publicado en Logical Methods in Computer Science (Volume 12, Issue 2).
El código de las correspondientes teorías en Coq se encuentra aquí.
Se ha publicado un artículo de razonamiento formalizado en Coq sobre semántica de lenguajes de programación titulado Flag-based big-step semantics.
Sus autores son
Su resumen es
Structural operational semantic specifications come in different styles: small-step and big-step. A problem with the big-step style is that specifying divergence and abrupt termination gives rise to annoying duplication. We present a novel approach to representing divergence and abrupt termination in big-step semantics using status flags. This avoids the duplication problem, and uses fewer rules and premises for representing divergence than previous approaches in the literature.
El trabajo se ha desarrollado en el proyecto PLanCompS (Programming Language Components and Specifications).
El código de las correspondientes teorías en Coq se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.
Se ha publicado un artículo de razonamiento formalizado en Coq sobre álgebra titulado Formalization of a Newton series representation of polynomials.
Sus autores son Cyril Cohen y Boris Djalal (del grupo Marelle en Inria Sophia Antipolis, Francia)
Su resumen es
We formalize an algorithm to change the representation of a polynomial to a Newton power series. This provides a way to compute efficiently polynomials whose roots are the sums or products of roots of other polynomials, and hence provides a base component of efficient computation for algebraic numbers. In order to achieve this, we formalize a notion of truncated power series and develop an abstract theory of poles of fractions.
El trabajo se ha presentado en el CPP 2016 (The 5th ACM SIGPLAN Conference on Certified Programs and Proofs).
El código de las correspondientes teorías en Coq se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.
Se ha publicado un artículo de razonamiento formalizado en Coq sobre teoría de números titulado Formal proofs of transcendence for e and π as an application of multivariate and symmetric polynomials.
Sus autores son
Su resumen es
We describe the formalisation in Coq of a proof that the numbers e and π are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of π relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.
El trabajo se presentará el 18 de enero de 2016 en el CPP 2016 (The 5th ACM SIGPLAN Conference on Certified Programs and Proofs).
El código de las correspondientes teorías en Coq se encuentra aquí.