Concrete semantics (A proof assistant approach)

PorJosé A. Alonso

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

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

Aliasing restrictions of C11 formalized in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre la semántica del lenguaje C titulado Aliasing restrictions of C11 formalized in Coq.

Su autor es Robbert Krebbers (de la Radboud University Nijmegen, Holanda).

Su resumen es

The C11 standard of the C programming language describes dynamic typing restrictions on memory operations to make more effective optimizations based on alias analysis possible. These restrictions are subtle due to the low-level nature of C, and have not been treated in a formal semantics before. We present an executable formal memory model for C that incorporates these restrictions, and at the same time describes required low-level operations.

Our memory model and essential properties of it have been fully formalized using the Coq proof assistant.

Este trabajo forma parte del proyecto CH₂O cuyo objetivo es la formalización del estándard C11 del lenguaje de programación C.

El trabajo se presentará en el CPP 2013 (3rd International Conference on Certified Programs and Proofs).

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

Formalizing probabilistic noninterference

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Formalizing probabilistic noninterference

Sus autores son Andrei Popescu, Johannes Hölzl y Tobias Nipkow (de la Universidad Técnica de Munich, Alemania).

Su resumen es

We present an Isabelle formalization of probabilistic noninterference for a multi-threaded language with uniform scheduling. Unlike in previous settings from the literature, here probabilistic behavior comes from both the scheduler and the individual threads, making the language more realistic and the mathematics more challenging. We study resumption-based and trace-based notions of probabilistic noninterference and their relationship, and also discuss compositionality w.r.t. the language constructs and type-system-like syntactic criteria. The formalization uses recent development in the Isabelle probability theory library.

El trabajo se presentará en el CPP 2013 (3rd International Conference on Certified Programs and Proofs).

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

Refinements for free!

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre refinamientos de datos titulado Refinements for free!.

Sus autores son

Su resumen es

Formal verification of algorithms often requires a choice between definitions that are easy to reason about and definitions that are computationally efficient. One way to reconcile both consists in adopting a high-level view when proving correctness and then refining stepwise down to an efficient low-level implementation. Some refinement steps are interesting, in the sense that they improve the algorithms involved, while others only express a switch from data representations geared towards proofs to more efficient ones geared towards computations. We relieve the user of these tedious refinements by introducing a framework where correctness is established in a proof-oriented context and automatically transported to computation-oriented data structures. Our design is general enough to encompass a variety of mathematical objects, such as rational numbers, polynomials and matrices over refinable structures. Moreover, the rich formalism of the Coq proof assistant enables us to develop this within Coq, without having to maintain an external tool.

El trabajo se presentará en el CPP 2013 (3rd International Conference on Certified Programs and Proofs).

Certified Kruskal’s tree theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre órdenes titulado Certified Kruskal’s tree theorem.

Su autor es Christian Sternagel (del Japan Advanced Institute of Science and Technology).

Su resumen es

This paper gives the first formalization of Kruskal’s tree theorem in a proof assistant. More concretely, an Isabelle/HOL development of Nash-Williams’ minimal bad sequence argument for proving the tree theorem is presented. Along the way, the proofs of Dickson’s lemma and Higman’s lemma are discussed.

El trabajo se presentará en el CPP 2013 (3rd International Conference on Certified Programs and Proofs).

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