Events and news relevant to the Laboratory for Foundations of Computer Science

[Andreas Abel <abela@chalmers.se>]

Slides of the talk (and draft paper) available at

  https://www.cse.chalmers.se/~abela/talks.html#edi25

On 2025-06-17 12:00, Ohad Kammar wrote:
> Hi,
>
> Reminding this week's LFCS seminar is about to start:
>
>    Tuesday, 17 Jun, 11.10am
>    (note unusal time)
>    Andreas Abel, Gothenburg University / Chalmers
>
>    The seminar will take place in-person only.
>
>    Andreas is visiting us for the week, and we will host him in office
>    IF 3.47. Please coordinate with him directly or with his host,
>    Nachi Valliappan <nachi.v@ed.ac.uk>
>
>
> We're synchronising the seminar time with the teaching timetable, and
> plan to start the talk at the advertised time, so please arrive a minute 
> or two
> earlier.
>
>
> In detail:
>
> ----------------------------------------------------------------------
> Andreas Abel, Gothenburg University / Chalmers
> https://www.cse.chalmers.se/~abela/
>
>    Tue, 17 Jun, 11.10am
>    (note unusual time)
>    Venue: IF G.03
>
>
> Title: Graded Call-by-push-value -- tracking (co)effects in a functional 
> language
>
> Abstract
>
>
> Call-by-push-value (CBPV) is a simply typed lambda calculus that
> polarizes types into value and computation types and can thus
> express both call-by-name and call-by-value evaluation in the
> presence of effects.  Semantically, effects are modeled by a monad,
> and computation types as algebras over this monad.
>
> Effect type systems usually express more information than the
> presence of an effect; often effects are categorized by a preordered
> monoid where the monoid operation represents accumulation of effects
> and the order expresses effect subsumption, in analogy to subtyping.
> In this work, a graded version of CBPV is presented where the
> typing of computations likens effect typing.  Semantically,
> computation types are then represented as graded monad algebras.
>
> Observing that the value types of CBPV can be interpreted as comonad
> coalgebras, we further present a version of CBPV that has coeffects
> graded by a preordered semiring.  Value types and contexts are
> interpreted as graded comonad coalgebras, allowing resource-aware
> interpretations of CBPV.
>
> Finally, we combine the two systems into a fully graded version of
> CBPV where both effects and coeffects are graded.  This turns out to
> be possible without specifying any interaction between effects and
> coeffects.