Showing 1–13 of 13 results for author: Tsampas, S

Higher-Order Mathematical Operational Semantics

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory… ▽ More Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term \emph{(pointed) higher-order GSOS laws}. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of combinatory logics and the $λ$-calculus w.r.t.\ a strong variant of Abramsky's applicative bisimilarity are obtained as instances. △ Less

Submitted 28 May, 2024; v1 submitted 26 May, 2024; originally announced May 2024.

Comments: Submitted to J. Funct. Program. Extended and updated version of arXiv:2210.13387

Bialgebraic Reasoning on Higher-Order Program Equivalence

Authors: Sergey Goncharov, Stefan Milius, Stelios Tsampas, Henning Urbat

Abstract: Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mat… ▽ More Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mathematical Operational Semantics, a highly parametric categorical framework for modeling the operational semantics of higher-order languages. Our main result asserts that for languages whose weak operational model forms a lax bialgebra, the logical relation is automatically sound for contextual equivalence. Our abstract theory is shown to instantiate to combinatory logics and $λ$-calculi with recursive types, and to different flavours of contextual equivalence. △ Less

Submitted 16 May, 2024; v1 submitted 1 February, 2024; originally announced February 2024.

Logical Predicates in Higher-Order Mathematical Operational Semantics

Authors: Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical relations. We first observe that logical predicates are special cases of coalgebraic invariants on mixed-variance functors. We then introduce the notion of a locally maximal logical refinement of a given predicate, with a… ▽ More We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical relations. We first observe that logical predicates are special cases of coalgebraic invariants on mixed-variance functors. We then introduce the notion of a locally maximal logical refinement of a given predicate, with a view to enabling inductive reasoning, and identify sufficient conditions on the overall setup in which locally maximal logical refinements canonically exist. Finally, we develop induction-up-to techniques that simplify inductive proofs via logical predicates on systems encoded as (certain classes of) higher-order GSOS laws by identifying and abstracting away from their boiler-plate part. △ Less

Submitted 12 January, 2024; v1 submitted 11 January, 2024; originally announced January 2024.

Comments: Extended version

A Study on Indoor Noise Levels in a Set of School Buildings in Greece utilizing an IoT infrastructure

Authors: Georgios Mylonas, Lidia Pocero Fraile, Stelios Tsampas, Athanasios Kalogeras

Abstract: Monitoring noise pollution in urban areas in a more systematic manner has been gaining traction as a theme among the research community, especially with the rise of smart cities and the IoT. However, although it affects our everyday life in a profound way, monitoring indoor noise levels inside workplaces and public buildings has so far grabbed less of our attention. In this work, we report on nois… ▽ More Monitoring noise pollution in urban areas in a more systematic manner has been gaining traction as a theme among the research community, especially with the rise of smart cities and the IoT. However, although it affects our everyday life in a profound way, monitoring indoor noise levels inside workplaces and public buildings has so far grabbed less of our attention. In this work, we report on noise levels data produced by an IoT infrastructure installed inside 5 school buildings in Greece. Our results indicate that such data can help to produce a more accurate picture of the conditions that students and educators experience every day, and also provide useful insights in terms of health risks and aural comfort. △ Less

Submitted 6 September, 2023; originally announced September 2023.

Comments: Preprint submitted to the WSACC 2023 workshop, organized in the scope of the 9th IEEE International Smart Cities Conference 2023

Weak Similarity in Higher-Order Mathematical Operational Semantics

Authors: Henning Urbat, Stelios Tsampas, Sergey Goncharov, Stefan Milius, Lutz Schröder

Abstract: Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak simil… ▽ More Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak similarity, which is shown to instantiate to well-known concepts such as Abramsky's applicative similarity for the lambda-calculus. On the way, we develop several techniques of independent interest at the level of abstract categories, including relation liftings of mixed-variance bifunctors and higher-order GSOS laws, as well as Howe's method. △ Less

Submitted 28 September, 2023; v1 submitted 16 February, 2023; originally announced February 2023.

Towards a Higher-Order Mathematical Operational Semantics

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the pr… ▽ More Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term pointed higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the $λ$-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances. △ Less

Submitted 26 October, 2022; v1 submitted 24 October, 2022; originally announced October 2022.

Stateful Structural Operational Semantics

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We intr… ▽ More Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences. △ Less

Submitted 11 May, 2022; v1 submitted 22 February, 2022; originally announced February 2022.

Experiences from Using LoRa and IEEE 802.15.4 for IoT-enabled Classrooms

Authors: Lidia Pocero, Stelios Tsampas, Georgios Mylonas, Dimitrios Amaxilatis

Abstract: Several networking technologies targeting the IoT application space currently compete within the smart city domain, both in outdoor and indoor deployments. However, up till now, there is no clear winner, and results from real-world deployments have only recently started to surface. In this paper, we present a comparative study of 2 popular IoT networking technologies, LoRa and IEEE 802.15.4, withi… ▽ More Several networking technologies targeting the IoT application space currently compete within the smart city domain, both in outdoor and indoor deployments. However, up till now, there is no clear winner, and results from real-world deployments have only recently started to surface. In this paper, we present a comparative study of 2 popular IoT networking technologies, LoRa and IEEE 802.15.4, within the context of a research-oriented IoT deployment inside school buildings in Europe, targeting energy efficiency in education. We evaluate the actual performance of these two technologies in real-world settings, presenting a comparative study on the effect of parameters like the built environment, network quality, or data rate. Our results indicate that both technologies have their advantages, and while in certain cases both are perfectly adequate, in our use case LoRa exhibits a more robust behavior. Moreover, LoRa's characteristics make it a very good choice for indoor IoT deployments such as in educational buildings, and especially in cases where there are low bandwidth requirements. △ Less

Submitted 17 February, 2021; originally announced February 2021.

Comments: Preprint version of the paper submitted to 2019 European Conference on Ambient Intelligence, 13-15 November 2019, Rome, Italy (AmI 2019). DOI:10.1007/978-3-030-34255-5_13

Abstract Congruence Criteria for Weak Bisimilarity

Authors: Stelios Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, Frank Piessens

Abstract: We introduce three general compositionality criteria over operational semantics and prove that, when all three are satisfied together, they guarantee weak bisimulation being a congruence. Our work is founded upon Turi and Plotkin's mathematical operational semantics and the coalgebraic approach to weak bisimulation by Brengos. We demonstrate each criterion with various examples of success and fail… ▽ More We introduce three general compositionality criteria over operational semantics and prove that, when all three are satisfied together, they guarantee weak bisimulation being a congruence. Our work is founded upon Turi and Plotkin's mathematical operational semantics and the coalgebraic approach to weak bisimulation by Brengos. We demonstrate each criterion with various examples of success and failure and establish a formal connection with the simply WB cool rule format of Bloom and van Glabbeek. In addition, we show that the three criteria induce lax models in the sense of Bonchi et al. △ Less

Submitted 13 October, 2021; v1 submitted 15 October, 2020; originally announced October 2020.

Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly

Authors: Carmine Abate, Matteo Busi, Stelios Tsampas

Abstract: The most prominent formal criterion for secure compilation is full abstraction, the preservation and reflection of contextual equivalence. Recent work introduced robust compilation, defined as the preservation of robust satisfaction of hyperproperties, i.e., their satisfaction against arbitrary attackers. In this paper, we initially set out to compare these two approaches to secure compilation. To… ▽ More The most prominent formal criterion for secure compilation is full abstraction, the preservation and reflection of contextual equivalence. Recent work introduced robust compilation, defined as the preservation of robust satisfaction of hyperproperties, i.e., their satisfaction against arbitrary attackers. In this paper, we initially set out to compare these two approaches to secure compilation. To that end, we provide an exact description of the hyperproperties that are robustly satisfied by programs compiled with a fully abstract compiler, and show that they can be meaningless or trivial. We then propose a novel criterion for secure compilation formulated in the framework of Mathematical Operational Semantics (MOS), guaranteeing both full abstraction and the preservation of robust satisfaction of hyperproperties in a more sensible manner. △ Less

Submitted 20 September, 2021; v1 submitted 26 June, 2020; originally announced June 2020.

Comments: Extended version of the APLAS'21 paper

CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle

Authors: Akram El-Korashy, Stelios Tsampas, Marco Patrignani, Dominique Devriese, Deepak Garg, Frank Piessens

Abstract: Capability machines such as CHERI provide memory capabilities that can be used by compilers to provide security benefits for compiled code (e.g., memory safety). The existing C to CHERI compiler, for example, achieves memory safety by following a principle called "pointers as capabilities" (PAC). Informally, PAC says that a compiler should represent a source language pointer as a machine code capa… ▽ More Capability machines such as CHERI provide memory capabilities that can be used by compilers to provide security benefits for compiled code (e.g., memory safety). The existing C to CHERI compiler, for example, achieves memory safety by following a principle called "pointers as capabilities" (PAC). Informally, PAC says that a compiler should represent a source language pointer as a machine code capability. But the security properties of PAC compilers are not yet well understood. We show that memory safety is only one aspect, and that PAC compilers can provide significant additional security guarantees for partial programs: the compiler can provide security guarantees for a compilation unit, even if that compilation unit is later linked to attacker-provided machine code. As such, this paper is the first to study the security of PAC compilers for partial programs formally. We prove for a model of such a compiler that it is fully abstract. The proof uses a novel proof technique (dubbed TrICL, read trickle), which should be of broad interest because it reuses the whole-program compiler correctness relation for full abstraction, thus saving work. We also implement our scheme for C on CHERI, show that we can compile legacy C code with minimal changes, and show that the performance overhead of compiled code is roughly proportional to the number of cross-compilation-unit function calls. △ Less

Submitted 4 May, 2021; v1 submitted 12 May, 2020; originally announced May 2020.

A categorical approach to secure compilation

Authors: Stelios Tsampas, Andreas Nuyts, Dominique Devriese, Frank Piessens

Abstract: We introduce a novel approach to secure compilation based on maps of distributive laws. We demonstrate through four examples that the coherence criterion for maps of distributive laws can potentially be a viable alternative for compiler security instead of full abstraction, which is the preservation and reflection of contextual equivalence. To that end, we also make use of the well-behavedness pro… ▽ More We introduce a novel approach to secure compilation based on maps of distributive laws. We demonstrate through four examples that the coherence criterion for maps of distributive laws can potentially be a viable alternative for compiler security instead of full abstraction, which is the preservation and reflection of contextual equivalence. To that end, we also make use of the well-behavedness properties of distributive laws to construct a categorical argument for the contextual connotations of bisimilarity. △ Less

Submitted 7 April, 2020; originally announced April 2020.

Comments: Accepted in Coalgebraic Methods in Computer Science, ver. 2020

A Methodology for Saving Energy in Educational Buildings Using an IoT Infrastructure

Authors: Georgios Mylonas, Dimitrios Amaxilatis, Stelios Tsampas, Lidia Pocero, Joakim Gunneriusson

Abstract: A considerable part of recent research in smart cities and IoT has focused on achieving energy savings in buildings and supporting aspects related to sustainability. In this context, the educational community is one of the most important ones to consider, since school buildings constitute a large part of non-residential buildings, while also educating students on sustainability matters is an inves… ▽ More A considerable part of recent research in smart cities and IoT has focused on achieving energy savings in buildings and supporting aspects related to sustainability. In this context, the educational community is one of the most important ones to consider, since school buildings constitute a large part of non-residential buildings, while also educating students on sustainability matters is an investment for the future. In this work, we discuss a methodology for achieving energy savings in schools based on the utilization of data produced by an IoT infrastructure installed inside school buildings and related educational scenarios. We present the steps comprising this methodology in detail, along with a set of tangible results achieved within the GAIA project. We also showcase how an IoT infrastructure can support activities in an educational setting and produce concrete outcomes, with typical levels of 20% energy savings. △ Less

Submitted 11 July, 2019; originally announced July 2019.

Comments: To appear in the 10th International Conference on Information, Intelligence, Systems and Applications (IISA 2019)