Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Sun 23 Aug 2020 12:30 - 13:00 at TyDe - Session 2

We introduce a novel dependent type theory called Graded Modal Dependent Type Theory (GrTT) that provides a new solution to the long-standing challenge of how to combine linear logic and dependent types. The key to reconciling these two notions is to leverage the recent approach of graded types, which treats data as a resource which is subject to fine-grained, quantitative tracking in the type system. GrTT offers fine-grained control over resource usage at both the runtime value level and the type level. We argue that the combination of linearity, graded modalities, and dependent types provides a rich language for specifying and reasoning about dependently-typed programs in a more fine-grained way than current approaches, enabling precise reasoning about usage information on compound data in a dependently-typed setting.

Towards Graded Modal Dependent Types (extended-abstract.pdf)80KiB

Sun 23 Aug

Displayed time zone: Eastern Time (US & Canada) change

12:30 - 14:00
Session 2TyDe at TyDe
12:30
30m
Talk
Graded Modal Dependent Type Theory (Extended Abstract)
TyDe
Benjamin Moon School of Computing, University of Kent, Harley D. Eades III Augusta University, Dominic Orchard University of Kent, UK
File Attached
13:00
30m
Talk
Frex: indexing modulo equations with free extensions (Extended Abstract)
TyDe
Guillaume Allais University of St Andrews, Edwin Brady University of St. Andrews, UK, Ohad Kammar University of Edinburgh, Jeremy Yallop University of Cambridge
13:30
30m
Talk
Retrofitting Symbolic Holes to LLVM IR (Extended Abstract)
TyDe
Bruce Collie University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh
Pre-print