Reseña: Mechanization of an algorithm for deciding KAT terms equivalence

PorJosé A. Alonso

Se ha publicado un nuevo trabajo sobre verificación formal en Coq: Mechanization of an algorithm for deciding KAT terms equivalence.

Sus autores son Nelma Moreira, David Pereira y Simao Melo de Sousa (de la Universidade do Porto, Portugal).

Su resumen es

This work presents a mechanically verified implementation of an algorithm for deciding the (in-)equivalence of Kleene algebra with tests (KAT) terms. This mechanization was carried out in the Coq proof assistant. The algorithm decides KAT terms equivalence through an iterated process of testing the equivalence of their partial derivatives. It is a purely syntactical decision procedure and so, it does not construct the underlying automata. The motivation for this work comes from the possibility of using KAT encoding of propositional Hoare logic for reasoning about the partial correctness of imperative programs.

El código de la formalización en Coq se encuentra aquí.

Meta-theory à la carte

PorJosé A. Alonso

Se ha publicado un nuevo artículo de automatización del razonamiento en Coq sobre metateorías de lenguajes de programación: Meta-theory à la carte.

Sus autores son Benjamin Delaware, Bruno C. d. S. Oliveira y Tom Schrijvers.

Su resumen es

Formalizing meta-theory, or proofs about programming languages, in a proof assistant has many well-known benefits. However, the considerable effort involved in mechanizing proofs has prevented it from becoming standard practice. This cost can be amortized by reusing as much of an existing formalization as possible when building a new language or extending an existing one. Unfortunately reuse of components is typically ad-hoc, with the language designer cutting and pasting existing definitions and proofs, and expending considerable effort to patch up the results.

This paper presents a more structured approach to the reuse of formalizations of programming language semantics through the composition of modular definitions and proofs. The key contribution is the development of an approach to induction for extensible Church encodings which uses a novel reinterpretation of the universal property of folds. These encodings provide the foundation for a framework, formalized in Coq, which uses type classes to automate the composition of proofs from modular components.

Several interesting language features, including binders and general recursion, illustrate the capabilities of our framework. We reuse these features to build fully mechanized definitions and proofs for a number of languages, including a version of mini-ML. Bounded induction enables proofs of properties for non-inductive semantic functions, and mediating type classes enable proof adaptation for more feature-rich languages.

El marco descrito en el artículo, así como el caso de estudio de mini-ML se encuentra en Meta-Theory à la Carte + Modular mini-ML.

Reseña: Lifting and transfer: A modular design for quotients in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un nuevo artículo sobre automatización del razonamiento en Isabelle/HOL: Lifting and transfer: A modular design for quotients in Isabelle/HOL.

Sus autores son Brian Huffman y Ondřej Kunčar (de la Technische Universität München).

El trabajo se presentará el 12 de agosto en el Isabelle Users Workshop 2012 en el marco del ITP 2012 (third conference on Interactive Theorem Proving).

Su resumen es

Quotients, subtypes, and other forms of type abstraction are ubiquitous in formal reasoning with higher-order logic. Typically, users want to build a library of operations and theorems about an abstract type, but they want to write definitions and proofs in terms of a more concrete representation type, or “raw” type. Earlier work on the Isabelle Quotient package [1, 2] has yielded great progress in automation, but it still has many technical limitations.

We present an improved, modular design centered around two new packages: the Transfer package for proving theorems, and the Lifting package for defining constants. Our new design is simpler, applicable in more situations, and has more user-friendly automation. An initial implementation is available in Isabelle 2012.

Reseña: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization

PorJosé A. Alonso

Esta semana se ha publicado en el Journal of Automated Reasoning un nuevo artículo de razonamiento formalizado en PVS: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization. Una versión previa se puede leer libremente aquí.

Los autores son César Muñoz y Anthony Narkawicz de NASA Langley Formal Methods.

Su resumen es

This paper presents a formalization in higher-order logic of an efficient representation of multivariate Bernstein polynomials. Using this representation, an algorithm for finding lower and upper bounds of the minimum and maximum values of a polynomial has been formalized and verified correct in the Prototype Verification System (PVS). The algorithm is used in the definition of proof strategies for formally and automatically solving polynomial global optimization problems.