Reseña: A new and formalized proof of abstract completion

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado A new and formalized proof of abstract completion.

Sus autores son

Su resumen es

Completion is one of the most studied techniques in term rewriting. We present a new proof of the correctness of abstract completion that is based on peak decreasingness, a special case of decreasing diagrams. Peak decreasingness replaces Newman’s Lemma and allows us to avoid proof orders in the correctness proof of completion. As a result, our proof is simpler than the one presented in textbooks, which is confirmed by our Isabelle/HOL formalization. Furthermore, we show that critical pair criteria are easily incorporated in our setting.

El trabajo se presentará el martes 15 de julio en el ITP 2014 (5th Conference on Interactive Theorem Proving).

El código de las correspondientes teorías en Isabelle/HOL es encuentra aquí.

Reseña: Towards a formally verified proof assistant

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Towards a formally verified proof assistant.

Sus autores son Abhishek Anand y Vincent Rahli (de la Cornell University).

Su resumen es

This paper presents a formalization of Nuprl’s metatheory in Coq. It includes a nominal-style definition of the Nuprl language, its reduction rules, a coinductive computational equivalence, and a Curry-style type system where a type is defined as a Partial Equivalence Relation (PER) à la Allen. This type system includes Martin-Löf dependent types, a hierarchy of universes, inductive types and partial types. We then prove that the typehood rules of Nuprl are valid w.r.t. this PER semantics and hence reduce Nuprl’s consistency to Coq’s consistency.

El trabajo se presentará el lunes 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í.

Reseña: Truly modular (co)datatypes for Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre automatización del razonamiento titulado Truly modular (co)datatypes for Isabelle/HOL.

Sus autores son

Su resumen es

“We extended Isabelle/HOL with a pair of definitional commands for datatypes and codatatypes. They support mutual and nested (co)recursion through well-behaved type constructors, including mixed recursion–corecursion, and are complemented by syntaxes for introducing primitively (co)recursive functions and by a general proof method for reasoning coinductively. As a case study, we ported Isabelle’s Coinductive library to use the new commands, eliminating the need for tedious ad hoc constructions.”

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

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

Reseña: Recursive functions on lazy lists via domains and topologies

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL Recursive functions on lazy lists via domains and topologies.

Sus autores son

Su resumen es

The usual definition facilities in theorem provers cannot handle all recursive functions on codatatypes; the filter function on lazy lists is a prime counterexample. We present two new ways of directly defining functions like filter by exploiting their dual nature as producers and consumers. Borrowing from domain theory and topology, we define them as a least fixpoint (producer view) and as a continuous extension (consumer view). Both constructions yield proof principles that allow elegant proofs.

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

Reseña: Cardinals in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre teoría de conjuntos titulado Cardinals in Isabelle/HOL.

Sus autores son Jasmin Christian Blanchette, Andrei Popescu y Dmitriy Traytel (de la Univ. Técnica de Munich).

Su resumen es

We report on a formalization of ordinals and cardinals in Isabelle/HOL. A main challenge we faced is the inability of higher-order logic to represent ordinals canonically, as transitive sets (as done in set theory). We resolved this into a “decentralized” representation that identifies ordinals with wellorders, with all concepts and results proved to be invariant under order isomorphism. We also discuss two applications of this general theory in formal developments.

El trabajo se presentará el martes 15 de julio en el ITP 2014 (5th Conference on Interactive Theorem Proving).