An Agda Formalization of a Graded Modal Type Theory with a Universe and Erasure

Hyperlinked rendering:

• ICFP 2023 Artefact

  This version is the basis for the publication A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized by Andreas Abel, Nils Anders Danielsson, and Oskar Eriksson, at The 28th ACM SIGPLAN International Conference on Functional Programming, Seattle, WA, USA, 4–9 September 2023.

• Development version (master)

Source repository: https://github.com/graded-type-theory/graded-type-theory