2 Search Results for "Koutavas, Vasileios"


Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Domain Reasoning in TopKAT

Authors: Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)


Abstract
TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the top element allows us to express the domain and codomain of a relation. This enables several applications in program logics, such as proving under-approximate specifications or reachability properties of imperative programs. However, while TopKAT inherits many pleasant features of KATs, such as having a decidable equational theory, it is incomplete with respect to relational models. In other words, there are properties that hold true of all relational TopKATs but cannot be proved with the axioms of TopKAT. This issue is potentially worrisome for program-logic applications, in which relational models play a key role. In this paper, we further investigate the completeness properties of TopKAT with respect to relational models. We show that TopKAT is complete with respect to (co)domain comparison of KAT terms, but incomplete when comparing the (co)domain of arbitrary TopKAT terms. Since the encoding of under-approximate specifications in TopKAT hinges on this type of formula, the aforementioned incompleteness results have a limited impact when using TopKAT to reason about such specifications.

Cite as

Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. Domain Reasoning in TopKAT. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 157:1-157:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ICALP.2024.157,
  author =	{Zhang, Cheng and de Amorim, Arthur Azevedo and Gaboardi, Marco},
  title =	{{Domain Reasoning in TopKAT}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{157:1--157:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.157},
  URN =		{urn:nbn:de:0030-drops-203003},
  doi =		{10.4230/LIPIcs.ICALP.2024.157},
  annote =	{Keywords: Kleene algebra, Kleene Algebra With Tests, Kleene Algebra With Domain, Kleene Algebra With Top and Tests, Completeness, Decidability}
}
Document
Limitations of Applicative Bisimulation (Preliminary Report)

Authors: Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)


Abstract
We present a series of examples that illuminate an important aspect of the semantics of higher-order functions with local state. Namely that certain behaviour of such functions can only be observed by pro- viding them with arguments that contain the functions themselves. This provides evidence for the necessity of complex conditions for functions in modern semantics for state, such as logical relations and Kripke-like bisimulations, where related functions are applied to related arguments (that may contain the functions). It also suggests that simpler semantics, such as those based on applicative bisimulations where functions are ap- plied to identical arguments, would not scale to higher-order languages with local state.

Cite as

Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. Limitations of Applicative Bisimulation (Preliminary Report). In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{koutavas_et_al:DagSemProc.10351.4,
  author =	{Koutavas, Vasileios and Levy, Paul Blain and Sumii, Eijiro},
  title =	{{Limitations of Applicative Bisimulation (Preliminary Report)}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.4},
  URN =		{urn:nbn:de:0030-drops-28074},
  doi =		{10.4230/DagSemProc.10351.4},
  annote =	{Keywords: Imperative languages, higher-order functions, local state}
}
  • Refine by Author
  • 1 Gaboardi, Marco
  • 1 Koutavas, Vasileios
  • 1 Levy, Paul Blain
  • 1 Sumii, Eijiro
  • 1 Zhang, Cheng
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Programming logic

  • Refine by Keyword
  • 1 Completeness
  • 1 Decidability
  • 1 Imperative languages
  • 1 Kleene Algebra With Domain
  • 1 Kleene Algebra With Tests
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2010
  • 1 2024