O raciocínio sobre equivalência de programas em linguagens imperativas é notoriamente desafiador, pois a presença de estados (na forma de armazenamentos de variáveis) aumenta fundamentalmente o poder observacional dos termos do programa. O desiderato chave para qualquer noção de equivalência é a composicionalidade, garantindo que subprogramas possam ser substituídos de forma segura por subprogramas equivalentes, independentemente do contexto. Para facilitar as provas de composicionalidade e evitar trabalho repetitivo, espera-se empregar os métodos bialgebráticos abstratos fornecidos pela poderosa teoria de semântica operacional matemática de Turi e Plotkin (também conhecida como GSOS abstrato) ou sua extensão recente por Goncharov et al. para linguagens de ordem superior. No entanto, várias tentativas de aplicar GSOS abstrato a linguagens com estado falharam até agora. Propomos uma nova abordagem para a semântica operacional de linguagens com estado baseada na distinção formal entre leitores (termos que esperam um armazenamento de entrada inicial antes de serem executados) e escritores (termos em execução que já receberam um armazenamento). Em contraste com trabalhos anteriores, este estilo de semântica é totalmente compatível com GSOS abstrato, e assim podemos aproveitar a teoria existente para obter técnicas de raciocínio coindutivas. Demonstramos que nossa abordagem gera resultados não triviais de composicionalidade para linguagens com estado com armazenamento de primeira e ordem superior e que se aplica de forma flexível a equivalências de programas em diferentes níveis de granularidade, como traço, custo e equivalência natural.
Goncharov et al. (Ter,) estudaram essa questão.