Stelios Tsampas

first.last at fau.de

Soon in Odense, Denmark

Hello! Nice to see you here :).

I am a Postdoctoral Researcher in the Theoretical Computer Science group at Friedrich-Alexander-Universität Erlangen-Nürnberg. Starting from February 2025, I will be a tenure-track Assistant Professor at the University of Southern Denmark (SDU), in the ACP Section.

I like working on the categorical foundations of computer science and applications thereof, currently focusing on programming languages and security, and more specifically on:

Foundations of Programming Languages
Formal Methods
Secure Compilation

I am actively developing the Higher-order Abstract GSOS (HO-GSOS) framework. The current running grant on HO-GSOS is ATLaS.

📰 news

Nov 08, 2024	Our paper Abstract Operational Methods for Call-by-Push-Value has been accepted for publication at POPL’25!
Jun 27, 2024	I am joining the ACP Section at the University of Southern Denmark (SDU) as a tenure-track Assistant Professor in early 2025.
Apr 15, 2024	Our paper Bialgebraic Reasoning on Higher-order Program Equivalence has been accepted for publication at LICS’24!
Dec 22, 2023	Our paper Logical Predicates in Higher-Order Mathematical Operational Semantics has been accepted for publication at FoSSaCS’24!
Aug 01, 2023	DFG Project ATLaS: Abstract Techniques for Programming Languages and Secure Compilation (~700K EUR) granted! The PIs are Sergey Goncharov and myself.

💬 latest talks

Sep 09, 2024	Higher-order Mathematical Operational Semantics, Aarhus University (Slides)
May 23, 2024	Logical Relations (and more) in Higher-order Mathematical Operational Semantics Invited talk, Chocola Meeting, Lyon (Slides)
Apr 10, 2024	Logical Predicates in Higher-order Mathematical Operational Semantics FoSSaCS’24, Luxembourg City (Slides)
Apr 04, 2024	Logical Predicates in Higher-order Mathematical Operational Semanticss WG6 Leuven (Abstract - Slides - Video)
Jan 20, 2023	Towards a Higher-Order Mathematical Operational Semantics POPL’23, Boston (Video)

🦉 selected publications

POPL

Abstract Operational Methods for Call-by-Push-Value

Sergey Goncharov, Stelios Tsampas, and Henning Urbat

Proc. ACM Program. Lang., Jan 2025

Abs DOI

Levy’s call-by-push-value is a comprehensive programming paradigm that combines elements from functional and imperative programming, supports computational effects and subsumes both call-by-value and call-by-name evaluation strategies. In the present work, we develop modular methods to reason about program equivalence in call-by-push-value, and in fine-grain call-by-value, which is a popular lightweight call-by-value sublanguage of the former. Our approach is based on the fundamental observation that presheaf categories of sorted sets are suitable universes to model call-by-(push)-value languages, and that natural, coalgebraic notions of program equivalence such as applicative similarity and logical relations can be developed within. Starting from this observation, we formalize fine-grain call-by-value and call-by-push-value in the higher-order abstract GSOS framework, reduce their key congruence properties to simple syntactic conditions by leveraging existing theory and argue that introducing changes to either language incurs minimal proof overhead.
LICS

Bialgebraic Reasoning on Higher-Order Program Equivalence

Sergey Goncharov, Stefan Milius, Stelios Tsampas, and Henning Urbat

In 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024), Jan 2024

DOI
LICS

Weak Similarity in Higher-Order Mathematical Operational Semantics

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

In 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2023), Jan 2023

DOI
POPL

Towards a Higher-Order Mathematical Operational Semantics

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

Proc. ACM Program. Lang., Jan 2023

Abs DOI

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.