Reseña: Certified HLints with Isabelle/HOLCF-Prelude

PorJosé A. Alonso

Se ha publicado un trabajo de verificación formal con Isabelle sobre Haskell titulado Certified HLints with Isabelle/HOLCF-Prelude.

Sus autores son Joachim Breitner, Brian Huffman, Neil Mitchell y Christian Sternagel.

El trabajo se presentará en el HART 2013 ( 1st International Workshop on Haskell And Rewriting Techniques).

Su resumen es

We present the HOLCF-Prelude, a formalization of a large part of Haskell’s standard prelude in Isabelle/HOLCF. Applying this formalization to the hints suggested by HLint allows us to certify them formally.

El códido del HOLCF-Prelude se encuentra aquí.

Reseña: Automatic data refinement

PorJosé A. Alonso

Se ha publicado un artículo de automatización del razonamiento en Isabelle/HOL titulado Automatic data refinement.

Su autor es Peter Lammich (de la Universidad Técnica de Munich).

El trabajo se presentará en julio en la ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

We present the Autoref tool for Isabelle/HOL, which automatically refines algorithms specified over abstract concepts like maps and sets to algorithms over concrete implementations like red-black-trees, and produces a refinement theorem. It is based on ideas borrowed from relational parametricity due to Reynolds and Wadler.

The tool allows for rapid prototyping of verified, executable algorithms. Moreover, it can be configured to fine-tune the result to the user’s needs. Our tool is able to automatically instantiate generic algorithms, which greatly simplifies the implementation of executable data structures.

Thanks to its integration with the Isabelle Refinement Framework and the Isabelle Collection Framework, Autoref can be used as a backend to a stepwise refinement based development approach, having access to a rich library of verified data structures. We have evaluated the tool by synthesizing efficiently executable refinements for some complex algorithms, as well as by implementing a library of generic algorithms for maps and sets.

La implementación de Autoref, junto con algunos casos de estudio, se encuentra aquí.

Reseña: The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups)

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre la demostración del teorema de Jordan-Hölder para grupos finitos titulado The rooster and the butterflies.

Su autora es Assia Mahboubi (de Microsoft Research – Inria Joint Centre).

El trabajo se presentará en julio en el CICM 2013 (Conferences on Intelligent Computer Mathematics).

Su resumen es

This paper describes a machine-checked proof of the Jordan-Hölder theorem for finite groups. This purpose of this description is to discuss the representation of the elementary concepts of finite group theory inside type theory. The design choices underlying these representations were crucial to the successful formalization of a complete proof of the Odd Order Theorem with the Coq system.

Reseña: Mechanical verification of SAT refutations with extended resolution

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en ACL2 titulado Mechanical verification of SAT refutations with extended resolution.

Sus autores son Nathan Wetzler, Marijn J. H. Heule y Warren A. Hunt Jr.

El trabajo se presentará en julio en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

We present a mechanically-verified proof checker developed with the ACL2 theorem-proving system that is general enough to support the growing variety of increasingly complex satisfiability (SAT) solver techniques, including those based on extended resolution. A common approach to assure the correctness of SAT solvers is to emit a proof of unsatisfiability when no solution is reported to exist. Contemporary proof checkers only check logical equivalence using resolution-style inference. However, some state-of-the-art, conflict-driven, clause-learning SAT solvers use preprocessing, inprocessing, and learning techniques, that cannot be checked solely by resolution-style inference. We have developed a mechanically-verified proof checker that assures refutation clauses preserve satisfiability. We believe our approach is sufficiently expressive to validate all known SAT-solver techniques.

Reseña: Type classes and filters for mathematical analysis in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre análisis matemático titulado Type classes and filters for mathematical analysis in Isabelle/HOL.

Sus autores son Johannes Hölzl, Fabian Immler y Brian Huffman.

El trabajo se presentará en julio en la ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

The theory of analysis in Isabelle/HOL derives from earlier formalizations that were limited to specific concrete types: ℝ, C and ℝⁿ. Isabelle’s new analysis theory unifies and generalizes these earlier efforts. The improvements are centered on two primary contributions: a generic theory of limits based on filters, and a new hierarchy of type classes that includes various topological, metric, vector, and algebraic spaces. These let us apply many results in multivariate analysis to types which are not Euclidean spaces, such as the extended real numbers, bounded continuous functions, or finite maps.