The Next 700 Relational Program Logics - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Proceedings of the ACM on Programming Languages Année : 2020

The Next 700 Relational Program Logics

Résumé

We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is highly expressive. At the semantic level, we provide an algebraic presentation of relational specifications as a class of relative monads, and link computations and specifications by introducing relational effect observations, which map pairs of monadic computations to relational specifications in a way that respects the algebraic structure. For an arbitrary relational effect observation, we generically define the core of a sound relational program logic, and explain how to complete it to a full-fledged logic for the monadic effect at hand. We show that this generic framework can be used to define relational program logics for effects as diverse as state, input-output, nondeterminism, and discrete probabilities. We, moreover, show that by instantiating our framework with state and unbounded iteration we can embed a variant of Benton's Relational Hoare Logic, and also sketch how to reconstruct Relational Hoare Type Theory. Finally, we identify and overcome conceptual challenges that prevented previous relational program logics from properly dealing with control effects, and are the first to provide a relational program logic for exceptions.
Fichier principal
Vignette du fichier
1907.05244 (1.16 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02398927 , version 1 (05-01-2024)

Identifiants

Citer

Kenji Maillard, Catalin Hritcu, Exequiel Rivas, Antoine van Muylder. The Next 700 Relational Program Logics. Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), ⟨10.1145/3371072⟩. ⟨hal-02398927⟩
102 Consultations
4 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More