| Lightweight semiformal time complexity analysis for purely functional data structures NA Danielsson ACM SIGPLAN Notices 43 (1), 133-144, 2008 | 132 | 2008 |
| Fast and loose reasoning is morally correct NA Danielsson, J Hughes, P Jansson, J Gibbons ACM SIGPLAN Notices 41 (1), 206-217, 2006 | 128 | 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 | 77 | 2012 |
| Subtyping, declaratively: An exercise in mixed induction and coinduction NA Danielsson, T Altenkirch Mathematics of Program Construction: 10th International Conference, MPC 2010 …, 2010 | 70 | 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 | 57 | 2011 |
| Isomorphism is equality T Coquand, NA Danielsson Indagationes Mathematicae 24 (4), 1105-1120, 2013 | 50 | 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 | 20 | 2009 |
| 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 | 14 | 2023 |
| Bag equivalence via a proof-relevant membership relation NA Danielsson Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012 | 14 | 2012 |
