Reseña: Formal proofs for nonlinear optimization

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Formal proofs for nonlinear optimization.

Sus autores son

Su resumen es

We present a formally verified global optimization framework. Given a semialgebraic or transcendental function f and a compact semialgebraic domain K, we use the nonlinear maxplus template approximation algorithm to provide a certified lower bound of f over K.

This method allows to bound in a modular way some of the constituents of f by suprema of quadratic forms with a well chosen curvature. Thus, we reduce the initial goal to a hierarchy of semialgebraic optimization problems, solved by sums of squares relaxations.

Our implementation tool interleaves semialgebraic approximations with sums of squares witnesses to form certificates. It is interfaced with Coq and thus benefits from the trusted arithmetic available inside the proof assistant. This feature is used to produce, from the certificates, both valid underestimators and lower bounds for each approximated constituent.

The application range for such a tool is widespread; for instance Hales’ proof of Kepler’s conjecture yields thousands of multivariate transcendental inequalities. We illustrate the performance of our formal framework on some of these inequalities as well as on examples from the global optimization literature.

El trabajo se ha publicado en el Journal of Formalized Reasoning.

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

Reseña: Mutual exclusion by four shared bits with not more than quadratic complexity

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en PVS sobre concurrencia titulado Mutual exclusion by four shared bits with not more than quadratic complexity.

Su autor es Wim H. Hesselink (de la Universidad de Groninga, Países Bajos).

Su resumen es

For years, the mutual exclusion algorithm of Lycklama and Hadzilacos (1991) was the optimal mutual exclusion algorithm with the first-come-first-served property, with a minimal number of (non-atomic) communication variables (5 bits per thread). Recently, Aravind published an improvement of it, which uses 4 bits per threads and has simplified waiting conditions. This algorithm is extended here with fault tolerance, and it is verified by assertional methods, using the proof assistant PVS. Progress is proved by means of UNITY logic. The paper proposes a new measure of concurrent time complexity, and proves that the concurrent complexity for throughput of the present algorithm is not more than quadratic in the number of threads.

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

Reseña: Bind induction: Extracting monadic programs from proofs

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre titulado Bind induction: Extracting monadic programs from proofs.

Sus autores son Hadi Shafei y James Caldwell (de la Univ. de Wyoming).

Su resumen es

Container types can be modeled as foldable monads that support the MonadPlus operations together with a membership operation. In this paper we present a new typeclass we call -Monad that supports a membership operator for instances of the MonadPlus typeclass. The laws for the -Monad typeclass specify how membership behaves with respect to the monad and monad plus operators. Using -Monads we are able write specifications of properties of generic containers. We also present an induction rule for monads we call bind induction. The new proof rule is proved to be sound. The computational content of the new induction rule is a bind operator, using this rule we are able to extract monadic programs from proofs. We present an example that uses the rule to extract a monadic program from a proof of a specification. We have used the Coq theorem prover to formalize the definitions presented here and to prove properties of the formalization. We rely on the Coq Type Class mechanism for our formalization.

El trabajo se ha presentado en el Symposium on Trends in Functional Programming 2014.

El código de las correspondientes teorías en Coq se encuentra en epsilon-Monad.v y decomposition.v.

Reseña: HOCore in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado HOCore in Coq.

Sus autores son

Su resumen es

We consider a recent publication on higher-order process calculi and describe how its results are formalized in the Coq proof assistant. We also highlight some important technical issues that we have uncovered in the original publication. We believe these issues are not unique to the paper under consideration, and require particular care to be avoided. Our ultimate goal is to show that it is possible to build a solid, high-confidence setting for formal reasoning on higher-order process calculi.

El trabajo se ha presentado en las Journées Francophones des Langages Applicatifs (JFLA 2015).

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