Menu Close

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

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.

Reseña