Reseña

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Experience implementing a performant category-theory library in Coq

Sus autores son Jason Gross, Adam Chlipala y David Spivak (del MIT).

Su resumen es

*We describe our experience implementing a broad category-theory library in Coq. Category theory and computational performance are not usually mentioned in the same breath, but we have needed substantial engineering effort to teach Coq to cope with large categorical constructions without slowing proof script processing unacceptably. In this paper, we share the lessons we have learned about how to represent very abstract mathematical objects and arguments in Coq and how future proof assistants might be designed to better support such reasoning. One particular encoding trick to which we draw attention allows category-theoretic arguments involving duality to be internalized in Coq’s logic with definitional equality. Ours may be the largest Coq development to date that uses the relatively new Coq version developed by homotopy type theorists, and we reflect on which new features were especially helpful. *

El trabajo se presentó el 14 de julio en el ITP 2014 (5th Conference on Interactive Theorem Proving).

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 metalógica titulado Completeness and decidability results for CTL in Coq.

Sus autores son Christian Doczkal y Gert Smolka (de la Saarland University, Saarbrücken).

Su resumen es

We prove completeness and decidability results for the temporal logic CTL in Coq/Ssreflect. Our basic result is a constructive proof that for every formula one can obtain either a finite model satisfying the formula or a proof in a Hilbert system certifying the unsatisfiability of the formula. The proof is based on a history-augmented tableau system obtained as the dual of Brünnler and Lange’s cut-free sequent calculus for CTL. We prove the completeness of the tableau system and give a translation of tableau refutations into Hilbert refutations. Decidability of CTL and completeness of the Hilbert system follow as corollaries.

El trabajo se presentará hoy en el ITP 2014 (5th Conference on Interactive Theorem Proving).

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 álgebra titulado A Coq formalization of finitely presented modules.

Sus autores son Cyril Cohen y Anders Mörtberg (de la University of Gothenburg).

Su resumen es

This paper presents a formalization of constructive module theory in the intuitionistic type theory of Coq. We build an abstraction layer on top of matrix encodings, in order to represent finitely presented modules, and obtain clean definitions with short proofs justifying that it forms an abelian category. The goal is to use it as a first step to compute certified topological invariants, like homology groups and Betti numbers.

El trabajo se presentará hoy en el ITP 2014 (5th Conference on Interactive Theorem Proving).

El código de las correspondientes teorías en Coq se encuentra aquí.