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

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

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

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

Subtyping, declaratively NA Danielsson, T Altenkirch International Conference on Mathematics of Program Construction, 100-118, 2010 | 54 | 2010 |

A formalisation of a dependently typed language as an inductive-recursive family NA Danielsson International Workshop on Types for Proofs and Programs, 93-109, 2006 | 52 | 2006 |

Parsing mixfix operators NA Danielsson, U Norell Symposium on Implementation and Application of Functional Languages, 80-99, 2008 | 41 | 2008 |

Chasing bottoms NA Danielsson, P Jansson International Conference on Mathematics of Program Construction, 85-109, 2004 | 40 | 2004 |

ΠΣ: Dependent types without the sugar T Altenkirch, NA Danielsson, A Löh, N Oury International Symposium on Functional and Logic Programming, 40-55, 2010 | 37 | 2010 |

Partiality, revisited T Altenkirch, NA Danielsson, N Kraus International Conference on Foundations of Software Science and Computation …, 2017 | 36 | 2017 |

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

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

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

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 | 18 | 2011 |

The agda wiki U Norell, NA Danielsson | 18 | 2005 |

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

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

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

Structurally recursive descent parsing NA Danielsson, U Norell Unpublished note, 2008 | 8* | 2008 |

Bag equivalence via a proof-relevant membership relation NA Danielsson International Conference on Interactive Theorem Proving, 149-165, 2012 | 6 | 2012 |