Isabell/HOL

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

Sus autores son

• Nao Hirokawa (del Japan Advanced Institute of Science and Technology, Japón),
• Aart Middeldorp (de la University of Innsbruck, Austria) y
• Christian Sternagel (de la University of Innsbruck, Austria)-

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í.

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

Sus autores son

• Andreas Lochbihler (del Institute of Information Security, ETH Zurich) y
• Johannes Hölzl (del Institut für Informatik, TU Müunchen).

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).

Se ha publicado un libro de razonamiento formalizado en Isabelle/HOL sobre semántica de lenguajes de programación titulado Concrete semantics (A proof assistant approach).

Sus autores son

• Tobias Nipkow (de la Univ. Técnica de Munich, Alemania) y
• Gerwin Klein (del NICTA, Australia).

Su resumen es

The book Concrete Semantics introduces semantics of programming languages through the medium of a proof assistant. The first part of the book is an introduction to the proof assistant Isabelle. The second part is an introduction to operational semantics and its applications and is based on a simple imperative programming language.

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