publications

2025

1. 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.

2024

1. 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
2. FoSSaCS

   Logical Predicates in Higher-Order Mathematical Operational Semantics

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

   In 27th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2024), Jan 2024

   DOI

2023

1. 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
2. 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.

2022

1. FSCD

   Stateful Structural Operational Semantics

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

   In 7th International Conference on Formal Structures for Computation and Deduction, FSCD’22, Jan 2022

   DOI

2021

1. IEEE CSF

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

   Akram El-Korashy, Stelios Tsampas, Marco Patrignani, Dominique Devriese, Deepak Garg, and 1 more author

   In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021, Jan 2021

   DOI
2. MFCS

   Abstract Congruence Criteria for Weak Bisimilarity

   Stelios Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, and Frank Piessens

   In 46th International Symposium on Mathematical Foundations of Computer Science, MFCS’21, Jan 2021

   DOI
3. APLAS

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

   Carmine Abate, Matteo Busi, and Stelios Tsampas

   In 19th Asian Symposium on Programming Languages and Systems, APLAS’21, Jan 2021

   DOI

2020

1. CMCS

   A Categorical Approach to Secure Compilation

   Stelios Tsampas, Andreas Nuyts, Dominique Devriese, and Frank Piessens

   In 15th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science, CMCS’20, Jan 2020

   DOI

2019

1. IEEE CSF

   Temporal Safety for Stack Allocated Memory on Capability Machines

   Stelios Tsampas, Dominique Devriese, and Frank Piessens

   In 32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019, Jan 2019

   DOI