Skip to content
Permalink
main
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

graded-haskell/README.md

Go to file
 
 
Cannot retrieve contributors at this time
Graded Haskell DDC GraD
47 lines (31 sloc) 2.04 KB
Raw Blame
Open in GitHub Desktop

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 available.

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.

A Virtual Box containing the Coq proof scripts is available.