Fri 20 Jan 2023 17:35 - 18:00 at Avenue34 - Semantics II Chair(s): Max S. New

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 \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 the SKI calculus and the $\lambda$-calculus w.r.t.\ a strong variant of Abramsky's applicative bisimilarity are obtained as instances.

Fri 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

16:45 - 18:00
Semantics IIPOPL at Avenue34
Chair(s): Max S. New University of Michigan
16:45
25m
Talk
Locally Nameless Sets
POPL
Andrew M. Pitts University of Cambridge
DOI Pre-print
17:10
25m
Talk
Why Are Proofs Relevant in Proof-Relevant Models?
POPL
Axel Kerinec Université Sorbonne Paris Nord; LIPN; CNRS, Giulio Manzonetto Université Sorbonne Paris Nord; LIPN; CNRS, Federico Olimpieri University of Leeds
DOI
17:35
25m
Talk
Towards a Higher-Order Mathematical Operational Semantics
POPL
Sergey Goncharov University of Erlangen-Nuremberg, Stefan Milius University of Erlangen-Nuremberg, Lutz Schröder University of Erlangen-Nuremberg, Stelios Tsampas University of Erlangen-Nuremberg, Henning Urbat University of Erlangen-Nuremberg
DOI Pre-print