
doi: 10.1145/3498680
handle: 11577/3510724 , 11568/1158206 , 11585/904238
Semantics is traditionally concerned with program equivalence, in which all pairs of programs which are not equivalent are treated the same, and simply dubbed as incomparable. In recent years, various forms of program metrics have been introduced such that the distance between non-equivalent programs is measured as an element of an appropriate quantale. By letting the underlying quantale vary as the type of the compared programs become more complex, the recently introduced framework of differential logical relations allows for a new contextual form of reasoning. In this paper, we show that all this can be generalised to effectful higher-order programs, in which not only the values , but also the effects computations produce can be appropriately distanced in a principled way. We show that the resulting framework is flexible, allowing various forms of effects to be handled, and that it provides compact and informative judgments about program differences.
Monads, Logical Relations; Program Distances; Lambda Calculus; Monads; Metrics, Lambda Calculus; Logical Relations; Metrics; Monads; Program Distances, Logical Relations Program Distances Lambda Calculus Monads Metrics, Program Distances, Metrics, Lambda Calculus, Logical Relations, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Monads, Logical Relations; Program Distances; Lambda Calculus; Monads; Metrics, Lambda Calculus; Logical Relations; Metrics; Monads; Program Distances, Logical Relations Program Distances Lambda Calculus Monads Metrics, Program Distances, Metrics, Lambda Calculus, Logical Relations, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 5 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
