Reseña: Abstract interpretation of annotated commands

El lunes (13 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Isabelle titulado Abstract interpretation of annotated commands.

Su autor es Tobias Nipkow (del Theorem Proving Group de la Technische Universität München).

El resumen del trabajo es

This paper formalises a generic abstract interpreter for a while-language, including widening and narrowing. The collecting semantics and the abstract interpreter operate on annotated commands: the program is represented as a syntax tree with the semantic information directly embedded, without auxiliary labels. The aim of the paper is simplicity of the formalisation, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics.

Las correspondientes teorías de Isabelle se encuentran aquí.