33 citations · 59 across the 4 of their papers we have counts for
Showing 2026Show all
2 papers · 1 filter
cs.PL2026
Erased Postulates, Identity Types and Quotients
Nils Anders Danielsson
This text is concerned with the question of whether, in type theory with erasure annotations, one can postulate that some type is inhabited and still have a guarantee that a progra…
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 …