ICFP 2026
Mon 24 - Sat 29 August 2026 Indianapolis, Indiana, United States
ICFP 2026 (series) / ICFP Artifacts /

An Agda Formalization of "On Recursion in Graded Modal Type Theory"

Oskar Eriksson, Andreas Abel, Nils Anders Danielsson
ICFP 2026 ICFP Artifacts

The artifact consists of Agda code which formalizes the results of the paper. The code uses the Agda standard library which needs to be installed for the code to type-check. The code has been tested using the latest versions of Agda (2.8.0) and the standard library (2.3). There are no other requirements to type-check the code.

small-avatar
Oskar Eriksson
Department of Computer Science and Engineering, University of Gothenburg and Chalmers University of Technology, Gothenburg, Sweden
Sweden
Andreas Abel
Andreas Abel
Gothenburg University
Sweden
small-avatar
Nils Anders Danielsson
University of Gothenburg
Sweden