2 papers
cs.LO2026
A Graded Modal Dependent Type Theory with Erasure, Formalized
Andreas Abel, Nils Anders Danielsson, Oskar Eriksson
We present a graded modal type theory, a dependent type theory with grades that can be used to enforce various properties of the code. The theory has -types, weak and strong …
cs.PL2024
Equivalence of Applicative Functors and Multifunctors
Andreas Abel
McBride and Paterson introduced Applicative functors to Haskell, which are equivalent to the lax monoidal functors (with strength) of category theory. Applicative functors F are pr…