2026-08-17T16:24:51Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17478 2024-03-06T11:00:04Z ddc:004 open_access

Open Higher-Order Logic Dal Lago, Ugo Gavazzo, Francesco Ghyselen, Alexis Formal Verification Relational Logic First-Order Properties We introduce a variation on Barthe et al.’s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity, differentiability, or monotonicity, can be expressed and reasoned about in a very natural way, following the structure of the underlying program. We give open higher-order logic in distinct flavors, and in particular in its relational and local versions, the latter being tailored for situations in which properties hold only in part of the underlying function’s domain of definition. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ugo Dal Lago and Francesco Gavazzo and Alexis Ghyselen 2023 Is Part Of LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2023.17 urn:nbn:de:0030-drops-174785 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.17 eng https://creativecommons.org/licenses/by/4.0/legalcode