Matroids from modules. - Nils Anders Danielsson; Michael B. Smyth (MFCSIT, 2002)

Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values. - Nils Anders Danielsson; Patrik Jansson (MPC, 2004)

Fast and loose reasoning is morally correct. - Nils Anders Danielsson; John Hughes 001; Patrik Jansson; Jeremy Gibbons (POPL, 2006)

A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family. - Nils Anders Danielsson (TYPES, 2006)

Functional Program Correctness Through Types. - Nils Anders Danielsson (2007)

Parsing Mixfix Operators. - Nils Anders Danielsson; Ulf Norell (IFL, 2008)

Lightweight semiformal time complexity analysis for purely functional data structures. - Nils Anders Danielsson (POPL, 2008)

PiSigma: Dependent Types without the Sugar. - Thorsten Altenkirch; Nils Anders Danielsson; Andres Löh; Nicolas Oury (FLOPS, 2010)

Total parser combinators. - Nils Anders Danielsson (ICFP, 2010)

Termination Checking in the Presence of Nested Inductive and Coinductive Types. - Thorsten Altenkirch; Nils Anders Danielsson (PAR@ITP, 2010)

Subtyping, Declaratively. - Nils Anders Danielsson; Thorsten Altenkirch (MPC, 2010)

Beating the Productivity Checker Using Embedded Languages - Nils Anders Danielsson (PAR, 2010)

Frontmatter, Table of Contents, Preface, Workshop Organization. - Nils Anders Danielsson; Bengt Nordström (TYPES, 2011)

Operational semantics using the partiality monad. - Nils Anders Danielsson (ICFP, 2012)

Bag Equivalence via a Proof-Relevant Membership Relation. - Nils Anders Danielsson (ITP, 2012)

Correct-by-construction pretty-printing. - Nils Anders Danielsson (DTP@ICFP, 2013)

Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type. - Thorsten Altenkirch; Nils Anders Danielsson; Nicolai Kraus (FoSSaCS, 2017)

Up-to techniques using sized types. - Nils Anders Danielsson (Proc. ACM Program. Lang., 2018)

Higher Inductive Type Eliminators Without Paths. - Nils Anders Danielsson (TYPES, 2019)

Practical dependent type checking using twin types. - Víctor López Juan; Nils Anders Danielsson (TyDe@ICFP, 2020)

Higher Lenses. - Paolo Capriotti; Nils Anders Danielsson; Andrea Vezzosi (LICS, 2021)

A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized. - Andreas Abel 001; Nils Anders Danielsson; Oskar Eriksson (Proc. ACM Program. Lang., 2023)