Meeting on Graded Types

17th June 2022 - School of Computing, University of Kent (+ online)

Graded type systems can be understood broadly as imbuing type systems with additional information that follows the underlying structure of a program or proof. This idea has grown considerably in recent years with various forms of graded type system being developed, for example, from generalisations of effect systems (modelled by graded monads), coeffect systems (modelled by graded comonads), quantitative type theories that generalise ideas from bounded linear logic, graded modal systems, contextual modal type theory, capability tracking systems, graded session types, adjoint logic and multi modal systems. In practical settings, graded type systems are becoming more prevalent, e.g., Granule, Idris 2, Haskell (via the LinearTypes extension).

The aim of this meeting is to bring together a wide variety of researchers working on such concepts across programming language theory and practice to report on latest work and share ideas. The hope is that this can be a pre-cursor to future such meetings, e.g., a Dagstuhl seminar.

Schedule

This is a hybrid event. You can attend in person or online. On Thursday afternoon, there is a separate but related event running, hosted by David Corfield, that all are welcome to attend as part of this:

  • Thursday 16th afternoon - 1-5pm - Grading in Philosophy, Linguistics and Computer Science

    Further details of this workshop

    • Linguistic targets for graded modalities

      Daniel Lassiter (University of Edinburgh)

    • Graded Modal Types for Fine-grained Program Reasoning

      Dominic Orchard (University of Kent and University of Cambridge)

    • Graded modalities and dependent type theory

      David Corfield (University of Kent)

  • Friday 17th - Meeting on Graded Types

    • A Mixed Linear and Graded Logic

      Harley Eades, (Augusta University)

    • Beyond semirings

      James Wood, (University of Strathclyde)

    • Graded Types For Extensible Dynamic Natural Language Semantics

      Jean-Philippe Bernardy (University of Gothenburg)

    • Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back
      Reasoning about the use of external resources is an important aspect of many practical applications. Effect systems enable tracking such information in types, but at the cost of complicating signatures of common functions. Capabilities coupled with escape analysis offer safety and natural signatures, but are often overly coarse grained and restrictive. We present SystemC, which builds on and generalizes ideas from type-based escape analysis and demonstrates that capabilities and effects can be reconciled harmoniously. By assuming that all functions are _second class_, we can admit natural signatures for many common programs. By introducing a notion of _boxed values_, we can lift the restrictions of second-class values at the cost of needing to track degree-of-impurity information in types. The system we present is expressive enough to support effect handlers in full capacity. We practically evaluate SystemC in an implementation and prove its soundness.

      Jonathan Brachthäuser (University of Tübingen)

    • From Ungraded to Graded: A Historical Perspective on Linear Type Systems

      Pritam Choudhury (University of Pennsylvania)

    • Title TBD Dylan McDermott (University of Reykjavik)

    • Title TBD Edwin Brady (University of St. Andrews)

    • Title TBD Andrew Hirsch (Max Planck Institute)

    • Short talk session
      • Unifying models of linear/graded dependent types Bob Atkey

Schedule TBD, but likely to last most of the day.

Signing up and attending in person

  • Sign up here
  • Please tick ‘In person’ if you would like to attend in person on the form.
  • The School of Computing at the University of Kent is about 30 minute walk from Canterbury West station, which is a bit less than an hour on the train from St. Pancras
  • There is a lot of accommodation nearby if you want to stay overnight. One recommendation is Acacia Lodge (which is near to the train station and again about 30 minutes walk from campus) or the Beverly Farmhouse (which is on campus).

  • Any questions please contact Dominic Orchard.