Search Results

Documents authored by Gavazzo, Francesco

Document
DOI: 10.4230/LIPIcs.LICS.2026.50
An Algebraic Approach to Formal System Metatheory

Authors: Francesco Gavazzo

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
We introduce an algebraic approach to the metatheory of formal systems of term assertions akin to those of structural and natural operational semantics, type theories, rewriting systems, and equational theories. We rest on Term Relation Algebras, viz. pointfree algebras of structurally-defined predicates on terms, to give a common algebraic semantics to different kinds of formal systems, regardless of their inferential mechanisms and underlying term structures. This enables abstract reasoning about formal systems, and their metatheory, through the algebra of the term predicates they define. We give a faithfully term-free algebraization of semantically-relevant term predicates, such as parallel reduction, big-step evaluation, and applicative bisimilarity. We extend this algebraization also to fundamental metatheoretical properties of these notions - including congruence of applicative bisimilarity, determinacy of evaluation, and confluence of reduction - and prove these properties using algebraic methods.
Cite as

Francesco Gavazzo. An Algebraic Approach to Formal System Metatheory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 50:1-50:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{gavazzo:LIPIcs.LICS.2026.50,
  author =	{Gavazzo, Francesco},
  title =	{{An Algebraic Approach to Formal System Metatheory}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{50:1--50:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.50},
  URN =		{urn:nbn:de:0030-drops-268379},
  doi =		{10.4230/LIPIcs.LICS.2026.50},
  annote =	{Keywords: Relation Algebra, Term Relations, Language Metatheory, Formal System Metatheory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.17
Open Higher-Order Logic

Authors: Ugo Dal Lago, Francesco Gavazzo, and Alexis Ghyselen

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

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.
Cite as

Ugo Dal Lago, Francesco Gavazzo, and Alexis Ghyselen. Open Higher-Order Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.CSL.2023.17},
  URN =		{urn:nbn:de:0030-drops-174785},
  doi =		{10.4230/LIPIcs.CSL.2023.17},
  annote =	{Keywords: Formal Verification, Relational Logic, First-Order Properties}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.3
A Fibrational Tale of Operational Logical Relations

Authors: Francesco Dagnino and Francesco Gavazzo

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages. However, a unifying abstract framework for operationally-based logical relations is still missing. We show how fibrations can provide a uniform treatment of operational logical relations, using as reference example a λ-calculus with generic effects endowed with a novel, abstract operational semantics defined on a large class of categories. Moreover, this abstract perspective allows us to give a solid mathematical ground also to differential logical relations - a recently introduced notion of higher-order distance between programs - both pure and effectful, bringing them back to a common picture with traditional ones.
Cite as

Francesco Dagnino and Francesco Gavazzo. A Fibrational Tale of Operational Logical Relations. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dagnino_et_al:LIPIcs.FSCD.2022.3,
  author =	{Dagnino, Francesco and Gavazzo, Francesco},
  title =	{{A Fibrational Tale of Operational Logical Relations}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.3},
  URN =		{urn:nbn:de:0030-drops-162840},
  doi =		{10.4230/LIPIcs.FSCD.2022.3},
  annote =	{Keywords: logical relations, operational semantics, fibrations, generic effects, program distance}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.23
Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs

Authors: Ugo Dal Lago and Francesco Gavazzo

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We investigate program equivalence for linear higher-order (sequential) languages endowed with primitives for computational effects. More specifically, we study operationally-based notions of program equivalence for a linear λ-calculus with explicit copying and algebraic effects à la Plotkin and Power. Such a calculus makes explicit the interaction between copying and linearity, which are intensional aspects of computation, with effects, which are, instead, extensional. We review some of the notions of equivalences for linear calculi proposed in the literature and show their limitations when applied to effectful calculi where copying is a first-class citizen. We then introduce resource transition systems, namely transition systems whose states are built over tuples of programs representing the available resources, as an operational semantics accounting for both intensional and extensional interactive behaviours of programs. Our main result is a sound and complete characterization of contextual equivalence as trace equivalence defined on top of resource transition systems.
Cite as

Ugo Dal Lago and Francesco Gavazzo. Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.FSCD.2021.23,
  author =	{Dal Lago, Ugo and Gavazzo, Francesco},
  title =	{{Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{23:1--23:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.23},
  URN =		{urn:nbn:de:0030-drops-142618},
  doi =		{10.4230/LIPIcs.FSCD.2021.23},
  annote =	{Keywords: algebraic effects, linearity, program equivalence, full abstraction}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.111
Differential Logical Relations, Part I: The Simply-Typed Case (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The novelty of differential logical relations consists in measuring the distance between terms not (necessarily) by a numerical value, but by a mathematical object which somehow reflects the interactive complexity, i.e. the type, of the compared terms. We exemplify this concept in the simply-typed lambda-calculus, and show a form of soundness theorem. We also see how ordinary logical relations and metric relations can be seen as instances of differential logical relations. Finally, we show that differential logical relations can be organised in a cartesian closed category, contrarily to metric relations, which are well-known not to have such a structure, but only that of a monoidal closed category.
Cite as

Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential Logical Relations, Part I: The Simply-Typed Case (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 111:1-111:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.ICALP.2019.111,
  author =	{Dal Lago, Ugo and Gavazzo, Francesco and Yoshimizu, Akira},
  title =	{{Differential Logical Relations, Part I: The Simply-Typed Case}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{111:1--111:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.111},
  URN =		{urn:nbn:de:0030-drops-106879},
  doi =		{10.4230/LIPIcs.ICALP.2019.111},
  annote =	{Keywords: Logical Relations, lambda-Calculus, Program Equivalence, Semantics}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact