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, doi: https://doi.org/10.1145/3607862.

• Licentiate Thesis 2025 Artefact

  This version is the basis for the licentiate thesis Graded Modal Type Theory, Formalized by Oskar Eriksson presented on May 8 2025, handle: https://hdl.handle.net/2077/86472.

• Development version (master)

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