| 2021 | LICS | Higher Lenses. | Paolo Capriotti, Nils Anders Danielsson, Andrea Vezzosi |
| 2020 | ICFP | Practical dependent type checking using twin types. | Vctor Lpez Juan, Nils Anders Danielsson |
| 2017 | FOSSACS | Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type. | Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus |
| 2013 | ICFP | Correct-by-construction pretty-printing. | Nils Anders Danielsson |
| 2012 | ICFP | Operational semantics using the partiality monad. | Nils Anders Danielsson |
| 2012 | ITP | Bag Equivalence via a Proof-Relevant Membership Relation. | Nils Anders Danielsson |
| 2010 | FLOPS | PiSigma: Dependent Types without the Sugar. | Thorsten Altenkirch, Nils Anders Danielsson, Andres Lh, Nicolas Oury |
| 2010 | ICFP | Total parser combinators. | Nils Anders Danielsson |
| 2010 | ITP | Termination Checking in the Presence of Nested Inductive and Coinductive Types. | Thorsten Altenkirch, Nils Anders Danielsson |
| 2010 | ITP | Beating the Productivity Checker Using Embedded Languages. | Nils Anders Danielsson |
| 2010 | MPC | Subtyping, Declaratively. | Nils Anders Danielsson, Thorsten Altenkirch |
| 2008 | POPL | Lightweight semiformal time complexity analysis for purely functional data structures. | Nils Anders Danielsson |
| 2006 | POPL | Fast and loose reasoning is morally correct. | Nils Anders Danielsson, John Hughes, Patrik Jansson, Jeremy Gibbons |
| 2004 | MPC | Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values. | Nils Anders Danielsson, Patrik Jansson |