Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Wed 21 Aug 2019 14:37 - 15:00 at Aurora Borealis - Modal Types Chair(s): Dominique Devriese

In programming, some data acts as a resource (e.g., file handles, channels) subject to usage constraints. This poses a challenge to software correctness as most languages are agnostic to constraints on data. The approach of linear types provides a partial remedy, delineating data into resources to be used but never copied or discarded, and unconstrained values. Bounded Linear Logic provides a more fine-grained approach, quantifying non-linear use via an indexed-family of modalities. Recent work on coeffect types generalises this idea to graded comonads, providing type systems which can capture various program properties. Here, we propose the umbrella notion of graded modal types, encompassing coeffect types and dual notions of type-based effect reasoning via graded monads. In combination with linear and indexed types, we show that graded modal types provide an expressive type theory for quantitative program reasoning, advancing the reach of type systems to capture and verify a broader set of program properties. We demonstrate this approach via a type system embodied in a fully-fledged functional language called Granule, exploring various examples.

Wed 21 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Modal TypesResearch Papers at Aurora Borealis
Chair(s): Dominique Devriese Vrije Universiteit Brussel
13:30
22m
Talk
Implementing a Modal Dependent Type TheoryDistinguished Paper
Research Papers
Daniel Gratzer Aarhus University, Jonathan Sterling Carnegie Mellon University, Lars Birkedal Aarhus University
13:52
22m
Talk
A Reasonably Exceptional Type Theory
Research Papers
Pierre-Marie Pédrot INRIA, Nicolas Tabareau Inria, Hans Fehrmann University of Chile, Éric Tanter University of Chile & Inria Paris
14:15
22m
Talk
Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming Without Space Leaks
Research Papers
Patrick Bahr IT University of Copenhagen, Christian Uldal Graulund IT University of Copenhagen, Rasmus Ejlers Møgelberg IT University of Copenhagen
14:37
22m
Talk
Quantitative program reasoning with graded modal types
Research Papers
Dominic Orchard University of Kent, UK, Vilem-Benjamin Liepelt University of Kent, UK, Harley D. Eades III Augusta University
Pre-print