This program is tentative and subject to change.

Graded types provide a way to augment a type system with fine-grained information, e.g., to track side effects or context dependence and resource use (called coeffects). Graded types for coeffects have found their way into languages such as Haskell, Idris, and Granule, enabling resourceful reasoning via coeffect analysis with varying levels of generality. Two separate lineages of graded coeffect system have emerged in the last decade: those in which coeffect annotations are pervasive, requiring annotations on function types (which we call graded-base) and those in which coeffects are added by way of a graded modal type operator atop linear types (which we call linear-base). The latter has its origins in Girard’s Linear Logic which has been a rich humus for programming language research focused on resources, whereas the graded-base approach emerged in the mid-2010s, seeing rapid adoption in programming language theory and practice, e.g. in QTT and Linear Haskell. The relationship between these two styles has however remained an open question. We answer this question by giving translations between pairs of calculi of both lineages that we prove type-, grade- and operational-semantics preserving. We show that the same notions of context dependence can be expressed in either style, building a bridge between the two lineages that enables transfer of results and ideas, while helping language designers to make better informed choices.

This program is tentative and subject to change.

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
Hide past events