En la clase de hoy del curso de Razonamiento automático se ha presentado la programación funcional en Isabelle/HOL.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2014: Programación funcional con Isabelle/HOL”
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Real-valued special functions: upper and lower bounds
Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).
Su resumen es
This development proves upper and lower bounds for several familiar real-valued functions. For sin, cos, exp and sqrt, it defines and verifies infinite families of upper and lower bounds, mostly based on Taylor series expansions. For arctan, ln and exp, it verifies a finite collection of upper and lower bounds, originally obtained from the functions’ continued fraction expansions using the computer algebra system Maple. A common theme in these proofs is to take the difference between a function and its approximation, which should be zero at one point, and then consider the sign of the derivative. The immediate purpose of this development is to verify axioms used by MetiTarski, an automatic theorem prover for real-valued special functions. Crucial to MetiTarski’s operation is the provision of upper and lower bounds for each function of interest.
El trabajo se ha publicado en en AFP (The Archive of Formal Proofs).
El código de las correspondientes teorías se encuentra aquí.
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Amortized complexity verified.
Su autor es Tobias Nipkow (de la Technische Universität München).
Su resumen es
*A framework for the analysis of the amortized complexity of (functional) data structures is formalized in Isabelle/HOL and applied to two non-trivial examples: skew heaps and splay trees. In the same spirit we show that the move-to-front algorithm for the list update problem is 2-competitive. *
El trabajo se presentó en el Isabelle Workshop 2014.
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
Se ha publicado un artículo de razonamiento formalizado titulado Interactive theorem provers from the perspective of Isabelle/Isar.
El autor es Makarius Wenzel (de la Univ. Paris-Sud, Prancia).
Su resumen es
Interactive Theorem Provers have a long tradition, going back to the 1970s when interaction was introduced as a concept in computing. The main provers in use today can be traced back over 20–30 years of development. As common traits there are usually strong logical systems at the bottom, with many layers of add-on tools around the logical core, and big applications of formalized mathematics or formal methods. There is a general attitude towards flexibility and open-endedness in the combination of logical tools: typical interactive provers use automated provers and dis-provers routinely in their portfolio.
The subsequent exposition of interactive theorem proving (ITP) takes Isabelle/Isar as the focal point to explain concepts of the greater “LCF family”, which includes Coq and various HOL systems. Isabelle itself shares much of the relatively simple logical foundations of HOL, but follows Coq in the ambition to deliver a sophisticated system to end-users without requiring self-assembly of individual parts. Isabelle today is probably the most advanced proof assistant concerning its overall architecture and extra-logical infrastructure.
The “Isar” aspect of Isabelle refers first to the structured language for human-readable and machine-checkable proof documents, but also to the Isabelle architecture that emerged around the logical framework in the past 10 years. Thus “Isabelle/Isar” today refers to an advanced proof assistant with extra structural integrity beyond the core logical framework, with native support for parallel proof processing and asynchronous interaction in its Prover IDE (PIDE).
El trabajo se presentó el 18 de julio en el APPA (All about Proofs, Proofs for All).
Se ha publicado un artículo de razonamiento formalizado en Isabelle titulado From operational models to information theory; side channels in pGCL with Isabelle.
Su autor es David Cock (del Software Systems Research Group, NICTA).
Su resumen es
In this paper, we formally derive the probabilistic security predicate (expectation) for a guessing attack against a system with side-channel leakage, modelled in pGCL. Our principal theoretical contribution is to link the process-oriented view, where attacker and system execute particular model programs, and the information-theoretic view, where the attacker solves an optimal-decoding problem, viewing the system as a noisy channel. Our practical contribution is to illustrate the selection of probabilistic loop invariants to verify such security properties, and the demonstration of a mechanical proof linking traditionally distinct domains.
El trabajo se presentó ayer en el ITP 2014 (5th Conference on Interactive Theorem Proving).
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.