2026-10-03T22:30:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7742 2024-03-06T09:41:01Z ddc:004 open_access

Type Systems for the Relational Verification of Higher Order Programs (Invited Talk) Gaboardi, Marco Relational verification refinement types type and effect systems complexity analysis Relational program verification is a variant of program verification where one focuses on guaranteeing properties about the executions of two programs, and as a special case about two executions of a single program on different inputs. Relational verification becomes particularly interesting when non-functional aspects of a computation, like probabilities or resource cost, are considered. Several approached to relational program verification have been developed, from relational program logics to relational abstract interpretation. In this talk, I will introduce two approaches to relational program verification for higher-order computations based on the use of type systems. The first approach consists in developing powerful type system where a rich language of assertions can be used to express complex relations between two programs. The second approach consists in developing more restrictive type systems enriched with effects expressing in a lightweight way relations between different runs of the same program. I will discuss the pros and cons of these two approaches on a concrete example: relational cost analysis, which aims at giving a bound on the difference in cost of running two programs, and as a special case the difference in cost of two executions of a single program on different inputs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Marco Gaboardi 2017 Is Part Of LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2017.1 urn:nbn:de:0030-drops-77429 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.1 eng https://creativecommons.org/licenses/by/3.0/legalcode