--------------------------------------------------------------------------
-- Code related to the licentiate thesis "Graded Modal Type Theory,
-- Formalized" by Oskar Eriksson.
--------------------------------------------------------------------------

-- Note that Andreas Abel, Nils Anders Danielsson, Gaëtan Gilbert,
-- Wojciech Nawrocki, Joakim Öhman and Andrea Vezzosi have also
-- contributed to the code, and some changes to the code were made after
-- feedback from anonymous reviewers.
--
-- The code also depends on some libraries:
--
-- * Agda's standard library, version 2.1.
-- * The builtin modules that are shipped with Agda 2.7.0.1.
--
-- When HTML code is generated from this file code is also generated
-- for the two libraries above, so URLs for their licences are
-- included here. At the time of writing the licence texts can be
-- found at the following URLs:
--
-- * https://github.com/agda/agda-stdlib/blob/v2.1/LICENCE
-- * https://github.com/agda/agda/blob/v2.7.0.1/LICENSE

module README where

-- Code related to Paper A: "A Graded Modal Dependent Type Theory
-- with a Universe and Erasure, Formalized" by Andreas Abel, Nils
-- Anders Danielsson and Oskar Eriksson.

import README.PaperA.README

-- Code related to Paper B: "A Resource-Correct Graded Modal Dependent
-- Type Theory with Recursion, Formalized" by Oskar Eriksson,
-- Nils Anders Danielsson and Andreas Abel.

import README.PaperB.README