Differential Program Semantics

Giving meaning to programs through axiomatic, denotational, and operational semantics is one of the main goals of theoretical computer science since its early days. Traditionally, program semantics is built around notions of program equivalence and refinement, based on which verification and transformation techniques can be justified. More and more often, however, programs are substituted with approximately equivalent programs, or verified against imprecise specifications. Program semantics has started dealing with program differences only in recent years, through the interpretation of programs in metric spaces. We give a brief survey about the state of the art on metric program semantics, and on the inadequacy of metrics as a way to deal with program differences. We thus point at a few preliminary results on a new kind of differential program semantics, which a soon-to-start ERC project plans to investigate along four axes: logical relations, bisimilarity, game se!mantics, and linear logic.