License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2023.17
URN: urn:nbn:de:0030-drops-174785
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17478/
Go to the corresponding LIPIcs Volume Portal

Dal Lago, Ugo ; Gavazzo, Francesco ; Ghyselen, Alexis

Open Higher-Order Logic

pdf-format:
LIPIcs-CSL-2023-17.pdf (0.9 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{dallago_et_al:LIPIcs.CSL.2023.17,
  author =	{Dal Lago, Ugo and Gavazzo, Francesco and Ghyselen, Alexis},
  title =	{{Open Higher-Order Logic}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{17:1--17:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/17478},
  URN =		{urn:nbn:de:0030-drops-174785},
  doi =		{10.4230/LIPIcs.CSL.2023.17},
  annote =	{Keywords: Formal Verification, Relational Logic, First-Order Properties}
}

Keywords: Formal Verification, Relational Logic, First-Order Properties
Collection: 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
Issue Date: 2023
Date of publication: 01.02.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI