Reseña: Flag-based big-step semantics
Se ha publicado un artículo de razonamiento formalizado en Coq sobre semántica de lenguajes de programación titulado Flag-based big-step semantics.
Sus autores son
- Casper Bach Poulsen (del Programming Languages Group en la Universidad Técnica de Delft en Delft Países Bajos), y
- Peter D. Mosses (del grupo Theoretical Computer Science en la Universidad de Swansea en Swansea, Gales, Reino Unido).
Su resumen es
Structural operational semantic specifications come in different styles: small-step and big-step. A problem with the big-step style is that specifying divergence and abrupt termination gives rise to annoying duplication. We present a novel approach to representing divergence and abrupt termination in big-step semantics using status flags. This avoids the duplication problem, and uses fewer rules and premises for representing divergence than previous approaches in the literature.
El trabajo se ha desarrollado en el proyecto PLanCompS (Programming Language Components and Specifications).
El código de las correspondientes teorías en Coq se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.