33 citations · 59 across the 4 of their papers we have counts for
4 papers
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…
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 …
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type
Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
Capretta's delay monad can be used to model partial computations, but it has the "wrong" notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay m…
Beating the Productivity Checker Using Embedded Languages
Nils Anders Danielsson
Some total languages, like Agda and Coq, allow the use of guarded corecursion to construct infinite values and proofs. Guarded corecursion is a form of recursion in which arbitrary…