ATLaS | Stelios Tsampas

The aim of the ATLaS project is to work on various important aspects of Higher-order Abstract GSOS. The project is funded by the Deutsche Forschungsgemeinschaft, the German Research Foundation, and will run from 01.2024 to 12.2026.

People

Main participants

Stelios Tsampas (co-PI)
Sergey Goncharov (co-PI)
Henning Urbat
Pouya Partow (PhD student)
Lutz Schröder
Stefan Milius

External collaborators

Alessio Santamaria, University of Sussex
Lars Birkedal, Aarhus University
Amin Timany, Aarhus University

Programme

Develop logical predicates in HO-GSOS ☑
Develop logical relations in HO-GSOS ☑
Apply our theory to develop new methods in call-by(-push)-value ☑
Big-step semantics for HO-GSOS ☐
Semantics for imperative languages ☐ (nearing completion)
Abstract approaches to parametricity ☐

Publications

Abstract Operational Methods for Call-by-Push-Value, POPL’25 [1]
Bialgebraic Reasoning on Higher-Order Program Equivalence, LICS’24 [2]
Logical Predicates in Higher-Order Mathematical Operational Semantics, FoSSaCS’24 [3]

Talks

Henning Urbat: Abstract operational methods for call-by-push-value
POPL’25, Denver, United States, January 2025.
Sergey Goncharov: Introduction to Higher-Order Mathematical Operational Semantics
Birmingham Theory Seminar, November 2024. Abstract - Slides.
Stelios Tsampas: Higher-order Mathematical Operational Semantics
Aarhus University visit, September 2024. Slides.
Henning Urbat: Bialgebraic reasoning on higher-order program equivalence
LICS’24, Tallinn, Estonia, July 2024. Slides.
Henning Urbat: Operational techniques for higher-order coalgebras
Dutch Categories and Types Seminar, Leiden, Netherlands, June 2024. Slides.
Sergey Goncharov: Higher-Order Program Equivalence in the Abstract
Research Seminar at Uni Regensburg, May 2024. Abstract - Slides.
Stelios Tsampas: Logical Relations (and more) in Higher-order Mathematical Operational Semantics
Chocola Meeting, Lyon, May 2024. (Invited talk). Slides.
Stelios Tsampas: Logical Predicates in Higher-order Mathematical Operational Semantics
FoSSaCS’24, Luxembourg City, Luxembourg, April 2024. Slides.
Stelios Tsampas: Logical Predicates in Higher-order Mathematical Operational Semantics
WG6 Leuven, April 2024. Abstract - Slides - Video.

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.

People

Main participants

External collaborators

Programme

Publications

Talks

References

2025

2024