Lightweight semiformal time complexity analysis for purely functional data structures NA Danielsson ACM SIGPLAN Notices 43 (1), 133-144, 2008 | 128 | 2008 |

Fast and loose reasoning is morally correct NA Danielsson, J Hughes, P Jansson, J Gibbons ACM SIGPLAN Notices 41 (1), 206-217, 2006 | 127 | 2006 |

Total parser combinators NA Danielsson Proceedings of the 15th ACM SIGPLAN international conference on Functional …, 2010 | 98 | 2010 |

Operational semantics using the partiality monad NA Danielsson Proceedings of the 17th ACM SIGPLAN international conference on Functional …, 2012 | 73 | 2012 |

Subtyping, declaratively: An exercise in mixed induction and coinduction NA Danielsson, T Altenkirch Mathematics of Program Construction: 10th International Conference, MPC 2010 …, 2010 | 69 | 2010 |

Partiality, revisited: The partiality monad as a quotient inductive-inductive type T Altenkirch, NA Danielsson, N Kraus International Conference on Foundations of Software Science and Computation …, 2017 | 63 | 2017 |

A formalisation of a dependently typed language as an inductive-recursive family NA Danielsson Types for Proofs and Programs: International Workshop, TYPES 2006 …, 2007 | 63 | 2007 |

Parsing mixfix operators NA Danielsson, U Norell Implementation and Application of Functional Languages: 20th International …, 2011 | 56 | 2011 |

Isomorphism is equality T Coquand, NA Danielsson Indagationes Mathematicae 24 (4), 1105-1120, 2013 | 47 | 2013 |

Chasing bottoms: A case study in program verification in the presence of partial and infinite values NA Danielsson, P Jansson International Conference on Mathematics of Program Construction, 85-109, 2004 | 47 | 2004 |

ΠΣ: Dependent types without the sugar T Altenkirch, NA Danielsson, A Löh, N Oury Functional and Logic Programming: 10th International Symposium, FLOPS 2010 …, 2010 | 45 | 2010 |

Beating the productivity checker using embedded languages NA Danielsson arXiv preprint arXiv:1012.4898, 2010 | 41 | 2010 |

Termination Checking in the Presence of Nested Inductive and Coinductive Types. T Altenkirch, NA Danielsson PAR@ ITP, 101-106, 2010 | 24* | 2010 |

Up-to techniques using sized types NA Danielsson Proceedings of the ACM on Programming Languages 2 (POPL), 1-28, 2017 | 22 | 2017 |

The agda wiki U Norell, NA Danielsson, A Abel, J Cockx | 21 | 2005 |

Correct-by-construction pretty-printing NA Danielsson Proceedings of the 2013 ACM SIGPLAN Workshop on Dependently-typed …, 2013 | 20 | 2013 |

The Agda standard library NA Danielsson, U Norell, SC Mu, S Bronson, D Doel, P Jansson, LT Chen Url: http://www. cs. nott. ac. uk/nad/repos/lib, 2011 | 20 | 2011 |

Mixing induction and coinduction NA Danielsson, T Altenkirch Draft paper, 2009 | 19 | 2009 |

Bag equivalence via a proof-relevant membership relation NA Danielsson Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012 | 14 | 2012 |

A graded modal dependent type theory with a universe and erasure, formalized A Abel, NA Danielsson, O Eriksson Proceedings of the ACM on Programming Languages 7 (ICFP), 920-954, 2023 | 9 | 2023 |