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

[Ohad Kammar <ohad.kammar@ed.ac.uk>]

Hi,

We'll have an LFCS seminar today:

  Tuesday, 17 Jun, 11.10am (note unusual 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.

----------------------------------------------------------------------

Upcoming seminars:

------------------

26 Jun: John Longley, Lecture 1, University of Edinburgh

27 Jun: John Longley, Lecture 2, University of Edinburgh

01 Jul: John Longley, Lecture 3, University of Edinburgh

08 Jul: John Longley, Lecture 4, University of Edinburgh

05 Aug: Michael Sperber, Active Group GmbH

If you would like to propose a speaker, or speak yourself, please contact me.

The seminar webpages:

http://web.inf.ed.ac.uk/lfcs/events/lfcs-seminars

Yours,

Ohad.

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.