I1M2014: 3º examen de programación con Haskell
Hoy se ha realizado el 3º examen del curso de Informática (de 1º de Grado en Matemáticas). Los ejercicios, y sus soluciones, se muestran a continuación.
Reseña: Depth-first search and strong connectivity in Coq
Se ha publicado un artículo de razonamiento formalizado en Coq sobre grafos titulado Depth-first search and strong connectivity in Coq.
Su autor es François Pottier (del grupo Gallium en el INRIA de Rocquencourt).
Su resumen es
Using Coq, we mechanize Wegener’s proof of Kosaraju’s linear-time algorithm for computing the strongly connected components of a directed graph. Furthermore, also in Coq, we define an executable and terminating depth-first search algorithm.
El trabajo se ha presentado en las Journées Francophones des Langages Applicatifs (JFLA 2015).
El código de las correspondientes teorías en Coq se encuentra aquí.
Reseña: MATHsAiD: Automated mathematical theory exploration
Se ha publicado un artículo de procesamiento del conocimiento matemático titulado MATHsAiD: Automated mathematical theory exploration.
Sus autores son
- Alan Bundy (de la Univ. de Edimburgo),
- Roy McCasland (de la Univ. de Edimburgo) y
- Patrick Smith (de la Univ. de Glasgow).
Su resumen es
The aim of the MATHsAiD project is to build a tool for automated theorem-discovery; to design and build a tool to automatically conjecture and prove theorems (lemmas, corollaries, etc.) from a set of user-supplied axioms and definitions. No other input is required. This tool would, for instance, allow a mathematician to try several versions of a particular definition, and in a relatively small amount of time, be able to see some of the consequences, in terms of the resulting theorems, of each version. Moreover, the automatically discovered theorems could perhaps help the users to discover and prove further theorems for themselves. The tool could also easily be used by educators (to generate exercise sets, for instance) and by students as well. In a similar fashion, it might also prove useful in enabling automated theorem provers to dispatch many of the more difficult proof obligations arising in software verification, by automatically generating lemma.
Reseña: LiquidHaskell: Refinement types in the real world
Se ha publicado un artículo sobre verificación de programas Haskell con LiquidHaskell titulado LiquidHaskell: Refinement types in the real world.
Sus autores son Niki Vazou, Eric L. Seidel y Ranjit Jhala (de la Univ. de California en San Diego).
Su resumen es
Haskell has many delightful features. Perhaps the one most beloved by its users is its type system that allows developers to specify and verify a variety of program properties at compile time. However, many properties, typically those that depend on relationships between program values are impossible, or at the very least, cumbersome to encode within the existing type system. Many such properties can be verified using a combination of Refinement Types and external SMT solvers. We describe the refinement type checker LiquidHaskell, that we have used to specify and verify a variety of properties of over 10,000 lines of Haskell code from various popular libraries, including containers, hscolour, bytestring, text, vector-algorithms and xmonad. First, we present a high-level overview of LiquidHaskell , through a tour of its features. Second, we present a qualitative discussion of the kinds of properties that can be checked – ranging from generic application independent criteria like totality and termination, to application specific concerns like memory safety and data structure correctness invariants. Finally, we present a quantitative evaluation of the approach, with a view towards measuring the efficiency and programmer’s effort required for verification, and discuss the limitations of the approach.
El trabajo se ha presentado en el ACM Haskell Symposium 2014.
Reseña: Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems
Se ha publicado un artículo de razonamiento formalizado en PVS titulado Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems
Sus autores son Anthony Narkawicz, César Muñoz y Aaron M. Dutle (del Formal Methods group en el NASA Langley Research Center).
Su resumen es
Sturm’s theorem is a well-known result in real algebraic geometry that provides a function that computes the number of roots of a univariate polynomial in a semi-open interval, not counting multiplicity. A generalization of Sturm’s theorem is known as Tarski’s theorem, which provides a linear relationship between functions known as Tarski queries and cardinalities of certain sets. The linear system that results from this relationship is in fact invertible and can be used to explicitly count the number of roots of a univariate polynomial on a set defined by a system of polynomial relations. This paper presents a formalization of these results in the PVS theorem prover, including formal proofs of Sturm’s and Tarski’s theorems. These theorems are at the basis of two decision procedures, which are implemented as computable functions in PVS. The first, based on Sturm’s theorem, determines satisfiability of a single polynomial relation over an interval. The second, based on Tarski’s theorem, determines the satisfiability of a system of polynomial relations over the real line. The soundness and completeness properties of these decision procedures are formally verified in PVS. The procedures and their correctness properties enable the implementation of PVS strategies for automatically proving existential and universal statements on polynomial systems. Since the decision procedures are formally verified in PVS, the soundness of the strategies depends solely on the internal logic of PVS rather than on an external oracle.
El trabajo se publicará en el Journal of Automated Reasoning.
El código de las correspondientes teorías en PVS del teorema de Sturm se encuentra aquí y el del teorema de Tarski aquí.