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 higherorder 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.

Ugo Dal Lago, Francesco Gavazzo (2022). Effectful program distancing. PROCEEDINGS OF ACM ON PROGRAMMING LANGUAGES, 6(POPL), 1-30 [10.1145/3498680].

Effectful program distancing

Ugo Dal Lago
;
Francesco Gavazzo
2022

Abstract

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 higherorder 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.
2022
Ugo Dal Lago, Francesco Gavazzo (2022). Effectful program distancing. PROCEEDINGS OF ACM ON PROGRAMMING LANGUAGES, 6(POPL), 1-30 [10.1145/3498680].
Ugo Dal Lago; Francesco Gavazzo
File in questo prodotto:
File Dimensione Formato  
popl2022a.pdf

accesso aperto

Tipo: Versione (PDF) editoriale
Licenza: Licenza per Accesso Aperto. Creative Commons Attribuzione - Condividi allo stesso modo (CCBYSA)
Dimensione 489.96 kB
Formato Adobe PDF
489.96 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/904238
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 3
social impact