The bialgebraic abstract GSOS framework by Turi and Plotkin provides an elegant categorical approach to modelling the operational and denotational semantics of programming and process languages. In abstract GSOS, bisimilarity is always a congruence, and it coincides with denotational equivalence. This saves the language designer from intricate, ad-hoc reasoning to establish these properties. The bialgebraic perspective on operational semantics in the style of abstract GSOS has recently been extended to higher-order languages, preserving compositionality of bisimilarity. However, a categorical understanding of bialgebraic denotational semantics according to Turi and Plotkin’s original vision has so far been missing in the higher-order setting. In the present paper, we develop a theory of adequate denotational semantics in higher-order abstract GSOS. The denotational models are parametric in an appropriately chosen semantic domain in the form of a locally final coalgebra for a behaviour bifunctor, whose construction is fully decoupled from the syntax of the language. Our approach captures existing accounts of denotational semantics such as semantic domains built via general step-indexing, previously introduced on a per-language basis, and is shown to be applicable to a wide range of different higher-order languages, e.g. simply typed and untyped languages, or languages with computational effects such as probabilistic or non-deterministic branching.

Tue 25 Aug

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

15:30 - 17:00
Types, Semantics, and Probabilistic ProgrammingICFP Papers at IP126 Auditorium
Chair(s): Leonidas Lampropoulos University of Maryland at College Park
15:30
18m
Talk
Another Type Inference Algorithm for First-class Implicit Polymorphism
ICFP Papers
J. Garrett Morris University of Iowa
DOI
15:48
18m
Talk
Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types
ICFP Papers
Vilem-Benjamin Liepelt University of Kent, UK, Danielle Marshall University of Glasgow, Dominic Orchard University of Cambridge; University of Kent
DOI
16:06
18m
Talk
Towards a Higher-Order Bialgebraic Denotational Semantics
ICFP Papers
Sergey Goncharov University of Birmingham, Marco Peressotti University of Southern Denmark, Stelios Tsampas University of Southern Denmark, Henning Urbat University of Erlangen-Nuremberg, Stefano Volpe University of Southern Denmark
DOI
16:24
18m
Talk
LazyHMC: Hamiltonian Monte Carlo simulation for lazy, infinite dimensional probabilistic programs
ICFP Papers
Maria-Nicoleta Craciun University of Oxford, C.-H. Luke Ong NTU, Tom Schrijvers KU Leuven, Sam Staton University of Oxford
DOI
16:42
18m
Talk
Imprecise Probabilistic Programming, Precisely (Functional Pearl)
ICFP Papers
Jack Liell-Cock University of Oxford, Sam Staton University of Oxford
DOI