Ugo Dal Lago, Università di Bologna
On Differential Program Semantics
Traditionally, program semantics is centered 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 recent results on a new kind of differential program semantics in which differences are somehow context-sensitive, and thus richer in structure than mere numbers.