Awesome

Graded Haskell

This repository contains mechanizations for two dependently-typed languages with graded types --- i.e. type systems where each variable in the context is annotated by some label drawn from an algebraic structure.

• DDC uses a lattice of dependency labels to track runtime and compiletime irrelevance
• GraD uses a semiring of grades to track resource usage

DDC

"A Dependent Dependency Calculus", paper by Pritam Choudhury, Harley Eades III, and Stephanie Weirich.
Published in ESOP 2022. The paper is part of the open-access proceedings (with a local copy here).

Pritam's ESOP 2022 video about this work (22 minutes).

Stephanie's Edinburgh seminar talk (June 2022).

The extended version of the paper, with the full appendix, is available from arXiv.

This repository proves type soundness for DDC, including the consistency of a grade-indexed definitional equivalence.

A Virtual Box containing the Coq proof scripts is archived on Zenodo.

GraD

"A Graded Dependent Type System with a Usage-Aware Semantics", by Pritam Choudhury, Harley Eades III, Richard A. Eisenberg and Stephanie Weirich. Published in POPL 2021 and available here (with a local copy here).

Pritam's POPL 2021 video about this work (30 minutes).

The extended version of the paper is available from arXiv.

This repository proves type soundness for GraD, assuming the consistency of an unspecified definitional equivalence.

The artifact has been archived in the ACM digital library.

A Virtual Box containing the Coq proof scripts is available.